| author | haftmann |
| Fri, 15 Feb 2013 08:31:31 +0100 | |
| changeset 51143 | 0a2371e7ced3 |
| parent 42842 | 6ef538f6a8ab |
| child 51160 | 599ff65b85e2 |
| permissions | -rw-r--r-- |
| 24195 | 1 |
|
| 31378 | 2 |
(* Author: Florian Haftmann, TU Muenchen *) |
3 |
||
4 |
header {* Generating code using pretty literals and natural number literals *}
|
|
| 24195 | 5 |
|
|
37695
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
31378
diff
changeset
|
6 |
theory Candidates_Pretty |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
42842
diff
changeset
|
7 |
imports Candidates Code_Char_ord Code_Target_Numeral |
| 24195 | 8 |
begin |
9 |
||
10 |
end |