src/HOL/ex/Codegenerator_Pretty.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 29933 125d513d9e39
child 31378 d1cbf6393964
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/Codegenerator_Pretty.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Simple examples for pretty numerals and such *}
     6 
     7 theory Codegenerator_Pretty
     8 imports ExecutableContent Code_Char Efficient_Nat
     9 begin
    10 
    11 declare isnorm.simps [code del]
    12 
    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