haftmann@24195: (*  Title:      HOL/ex/Codegenerator_Pretty.thy
haftmann@24195:     ID:         $Id$
haftmann@24195:     Author:     Florian Haftmann, TU Muenchen
haftmann@24195: *)
haftmann@24195: 
haftmann@24195: header {* Simple examples for pretty numerals and such *}
haftmann@24195: 
haftmann@24195: theory Codegenerator_Pretty
haftmann@25963: imports ExecutableContent Code_Char Efficient_Nat
haftmann@24195: begin
haftmann@24195: 
haftmann@26022: setup {*
haftmann@26022:   Code.del_funcs
haftmann@26022:     (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "index"}))
haftmann@26022:   #> Code.del_funcs
haftmann@26022:     (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "char"}))
haftmann@26022:   #> Code.del_funcs
haftmann@26022:     (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "int"}))
haftmann@26022:   #> Code.del_funcs
haftmann@26022:     (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "nat"}))
haftmann@26022: *}
haftmann@25933: 
haftmann@25963: declare char.recs [code func del]
haftmann@25963:   char.cases [code func del]
haftmann@25963:   char.size [code func del]
haftmann@24195: 
haftmann@25963: declare isnorm.simps [code func del]
haftmann@25933: 
haftmann@25963: ML {* (*FIXME get rid of this*)
haftmann@25963: nonfix union;
haftmann@25963: nonfix inter;
haftmann@25963: nonfix upto;
haftmann@25963: *}
haftmann@25933: 
haftmann@25963: export_code * in SML module_name CodegenTest
haftmann@25963:   in OCaml module_name CodegenTest file -
haftmann@25963:   in Haskell file -
haftmann@25616: 
haftmann@25963: ML {*
haftmann@25963: infix union;
haftmann@25963: infix inter;
haftmann@25963: infix 4 upto;
haftmann@25963: *}
haftmann@24195: 
haftmann@24195: end