equal
deleted
inserted
replaced
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 Predicate |
8 imports Plain Typerep Code_Numeral Predicate |
9 uses ("Tools/code_evaluation.ML") |
|
10 begin |
9 begin |
11 |
10 |
12 subsection {* Term representation *} |
11 subsection {* Term representation *} |
13 |
12 |
14 subsubsection {* Terms and class @{text term_of} *} |
13 subsubsection {* Terms and class @{text term_of} *} |
71 lemma eq_eq_TrueD: |
70 lemma eq_eq_TrueD: |
72 assumes "(x \<equiv> y) \<equiv> Trueprop True" |
71 assumes "(x \<equiv> y) \<equiv> Trueprop True" |
73 shows "x \<equiv> y" |
72 shows "x \<equiv> y" |
74 using assms by simp |
73 using assms by simp |
75 |
74 |
76 use "Tools/code_evaluation.ML" |
75 ML_file "Tools/code_evaluation.ML" |
77 |
76 |
78 code_reserved Eval Code_Evaluation |
77 code_reserved Eval Code_Evaluation |
79 |
78 |
80 setup {* Code_Evaluation.setup *} |
79 setup {* Code_Evaluation.setup *} |
81 |
80 |