src/HOL/ex/Codegenerator_Pretty.thy
changeset 26446 6abb5ed522a6
parent 26022 b30a342a6e29
child 26468 bb6a015219cf
equal deleted inserted replaced
26445:17223cf843d8 26446:6abb5ed522a6
    24   char.cases [code func del]
    24   char.cases [code func del]
    25   char.size [code func del]
    25   char.size [code func del]
    26 
    26 
    27 declare isnorm.simps [code func del]
    27 declare isnorm.simps [code func del]
    28 
    28 
       
    29 setup {*
       
    30 let
       
    31   val charr = @{const_name Char}
       
    32   val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
       
    33     @{const_name Nibble2}, @{const_name Nibble3},
       
    34     @{const_name Nibble4}, @{const_name Nibble5},
       
    35     @{const_name Nibble6}, @{const_name Nibble7},
       
    36     @{const_name Nibble8}, @{const_name Nibble9},
       
    37     @{const_name NibbleA}, @{const_name NibbleB},
       
    38     @{const_name NibbleC}, @{const_name NibbleD},
       
    39     @{const_name NibbleE}, @{const_name NibbleF}];
       
    40 in
       
    41   fold (fn target => CodeTarget.add_pretty_char target charr nibbles)
       
    42     ["SML", "OCaml", "Haskell"]
       
    43   #> CodeTarget.add_pretty_list_string "Haskell"
       
    44     @{const_name Nil} @{const_name Cons} charr nibbles
       
    45 end
       
    46 *}
       
    47 
    29 ML {* (*FIXME get rid of this*)
    48 ML {* (*FIXME get rid of this*)
    30 nonfix union;
    49 nonfix union;
    31 nonfix inter;
    50 nonfix inter;
    32 nonfix upto;
    51 nonfix upto;
    33 *}
    52 *}