src/HOL/ex/Codegenerator_Pretty.thy
author haftmann
Mon Feb 16 13:38:09 2009 +0100 (2009-02-16)
changeset 29933 125d513d9e39
parent 28663 bd8438543bf2
child 31378 d1cbf6393964
permissions -rw-r--r--
dropped Id
     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