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 Presburger |
9 imports Plain "~~/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 |