| author | haftmann |
| Fri, 10 Oct 2008 06:45:53 +0200 | |
| changeset 28562 | 4e74209f113e |
| parent 28335 | 25326092cf9a |
| child 28663 | bd8438543bf2 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/ex/Codegenerator_Pretty.thy
2 ID: $Id$
3 Author: Florian Haftmann, TU Muenchen
4 *)
6 header {* Simple examples for pretty numerals and such *}
8 theory Codegenerator_Pretty
9 imports ExecutableContent Code_Char Efficient_Nat
10 begin
12 declare isnorm.simps [code del]
14 ML {* (*FIXME get rid of this*)
15 nonfix union;
16 nonfix inter;
17 nonfix upto;
18 *}
20 export_code "RType.*" -- "workaround for cache problem"
21 export_code * in SML module_name CodegenTest
22 in OCaml module_name CodegenTest file -
23 in Haskell file -
25 ML {*
26 infix union;
27 infix inter;
28 infix 4 upto;
29 *}
31 end