equal
deleted
inserted
replaced
91 (OCaml "Big'_int.lt'_big'_int") |
91 (OCaml "Big'_int.lt'_big'_int") |
92 (Haskell infix 4 "<") |
92 (Haskell infix 4 "<") |
93 |
93 |
94 code_const Code_Numeral.int_of |
94 code_const Code_Numeral.int_of |
95 (SML "IntInf.fromInt") |
95 (SML "IntInf.fromInt") |
96 (OCaml "Big'_int.big'_int'_of'_int") |
96 (OCaml "_") |
97 (Haskell "toEnum") |
97 (Haskell "toEnum") |
98 |
98 |
99 code_reserved SML IntInf |
99 code_reserved SML IntInf |
100 code_reserved OCaml Big_int |
|
101 |
100 |
102 text {* Evaluation *} |
101 text {* Evaluation *} |
103 |
102 |
104 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term" |
103 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term" |
105 (Eval "HOLogic.mk'_number/ HOLogic.intT") |
104 (Eval "HOLogic.mk'_number/ HOLogic.intT") |