equal
deleted
inserted
replaced
90 code_reserved SML IntInf |
90 code_reserved SML IntInf |
91 code_reserved OCaml Big_int |
91 code_reserved OCaml Big_int |
92 |
92 |
93 text {* Evaluation *} |
93 text {* Evaluation *} |
94 |
94 |
95 lemma [code func, code func del]: |
95 lemma [code, code del]: |
96 "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" .. |
96 "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" .. |
97 |
97 |
98 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term" |
98 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term" |
99 (SML "HOLogic.mk'_number/ HOLogic.intT") |
99 (SML "HOLogic.mk'_number/ HOLogic.intT") |
100 |
100 |