equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Codegenerator_Pretty.thy |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
1 |
5 header {* Simple examples for pretty numerals and such *} |
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* Generating code using pretty literals and natural number literals *} |
6 |
5 |
7 theory Codegenerator_Pretty |
6 theory Codegenerator_Pretty |
8 imports ExecutableContent Code_Char Efficient_Nat |
7 imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat |
9 begin |
8 begin |
10 |
9 |
11 declare isnorm.simps [code del] |
10 declare isnorm.simps [code del] |
12 |
11 |
13 ML {* (*FIXME get rid of this*) |
|
14 nonfix union; |
|
15 nonfix inter; |
|
16 nonfix upto; |
|
17 *} |
|
18 |
|
19 export_code * in SML module_name CodegenTest |
|
20 in OCaml module_name CodegenTest file - |
|
21 in Haskell file - |
|
22 |
|
23 ML {* |
|
24 infix union; |
|
25 infix inter; |
|
26 infix 4 upto; |
|
27 *} |
|
28 |
|
29 end |
12 end |