changeset 32657 | 5f13912245ff |
parent 31377 | a48f9ef9de15 |
child 34899 | 8674bb6f727b |
32653:7feb35deb6f6 | 32657:5f13912245ff |
---|---|
98 |
98 |
99 code_reserved SML IntInf |
99 code_reserved SML IntInf |
100 |
100 |
101 text {* Evaluation *} |
101 text {* Evaluation *} |
102 |
102 |
103 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term" |
103 code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term" |
104 (Eval "HOLogic.mk'_number/ HOLogic.intT") |
104 (Eval "HOLogic.mk'_number/ HOLogic.intT") |
105 |
105 |
106 end |
106 end |