equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Pretty integer literals for code generation *} |
6 header {* Pretty integer literals for code generation *} |
7 |
7 |
8 theory Code_Integer |
8 theory Code_Integer |
9 imports Plain "~~/src/HOL/Presburger" |
9 imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger" |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 HOL numeral expressions are mapped to integer literals |
13 HOL numeral expressions are mapped to integer literals |
14 in target languages, using predefined target language |
14 in target languages, using predefined target language |
88 (Haskell infix 4 "<") |
88 (Haskell infix 4 "<") |
89 |
89 |
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 *} |
|
94 |
|
95 lemma [code func, code func del]: |
|
96 "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" .. |
|
97 |
|
98 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term" |
|
99 (SML "HOLogic.mk'_number/ HOLogic.intT") |
|
100 |
93 end |
101 end |