equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Pretty integer literals for code generation *} |
5 header {* Pretty integer literals for code generation *} |
6 |
6 |
7 theory Code_Integer |
7 theory Code_Integer |
8 imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger" |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 HOL numeral expressions are mapped to integer literals |
12 HOL numeral expressions are mapped to integer literals |
13 in target languages, using predefined target language |
13 in target languages, using predefined target language |