src/HOL/ex/Codegenerator_Pretty.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 26022 b30a342a6e29
child 26446 6abb5ed522a6
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     1 (*  Title:      HOL/ex/Codegenerator_Pretty.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 header {* Simple examples for pretty numerals and such *}
     7 
     8 theory Codegenerator_Pretty
     9 imports ExecutableContent Code_Char Efficient_Nat
    10 begin
    11 
    12 setup {*
    13   Code.del_funcs
    14     (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "index"}))
    15   #> Code.del_funcs
    16     (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "char"}))
    17   #> Code.del_funcs
    18     (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "int"}))
    19   #> Code.del_funcs
    20     (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "nat"}))
    21 *}
    22 
    23 declare char.recs [code func del]
    24   char.cases [code func del]
    25   char.size [code func del]
    26 
    27 declare isnorm.simps [code func del]
    28 
    29 ML {* (*FIXME get rid of this*)
    30 nonfix union;
    31 nonfix inter;
    32 nonfix upto;
    33 *}
    34 
    35 export_code * in SML module_name CodegenTest
    36   in OCaml module_name CodegenTest file -
    37   in Haskell file -
    38 
    39 ML {*
    40 infix union;
    41 infix inter;
    42 infix 4 upto;
    43 *}
    44 
    45 end