| changeset 46664 | 1f6c140f9c72 |
| parent 46638 | fc315796794e |
| child 47108 | 2a1953f0d20d |
| 46663:7fe029e818c2 | 46664:1f6c140f9c72 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Term evaluation using the generic code generator *} |
5 header {* Term evaluation using the generic code generator *} |
6 |
6 |
7 theory Code_Evaluation |
7 theory Code_Evaluation |
8 imports Plain Typerep Code_Numeral |
8 imports Plain Typerep Code_Numeral Predicate |
9 uses ("Tools/code_evaluation.ML") |
9 uses ("Tools/code_evaluation.ML") |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Term representation *} |
12 subsection {* Term representation *} |
13 |
13 |