equal
deleted
inserted
replaced
|
1 (* Title: thys/Recursive.thy |
|
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
|
3 *) |
|
4 |
|
5 header {* Translating Recursive Functions into Abacus Machines *} |
|
6 |
1 theory Recursive |
7 theory Recursive |
2 imports Rec_Def Abacus |
8 imports Rec_Def Abacus |
3 begin |
9 begin |
4 |
10 |
5 section {* Compiling from recursive functions to Abacus machines *} |
|
6 |
11 |
7 text {* |
12 text {* |
8 Some auxilliary Abacus machines used to construct the result Abacus machines. |
13 Some auxilliary Abacus machines used to construct the result Abacus machines. |
9 *} |
14 *} |
10 |
15 |