src/HOL/Library/Code_Char.thy
changeset 28090 29af3c712d2b
parent 28064 d4a6460c53d1
child 28228 7ebe8dc06cbb
equal deleted inserted replaced
28089:66ae1926482a 28090:29af3c712d2b
    23   (SML "char")
    23   (SML "char")
    24   (OCaml "char")
    24   (OCaml "char")
    25   (Haskell "Char")
    25   (Haskell "Char")
    26 
    26 
    27 setup {*
    27 setup {*
    28 let
    28   fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] 
    29   val charr = @{const_name Char}
    29   #> add_literal_list_string "Haskell"
    30   val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
       
    31     @{const_name Nibble2}, @{const_name Nibble3},
       
    32     @{const_name Nibble4}, @{const_name Nibble5},
       
    33     @{const_name Nibble6}, @{const_name Nibble7},
       
    34     @{const_name Nibble8}, @{const_name Nibble9},
       
    35     @{const_name NibbleA}, @{const_name NibbleB},
       
    36     @{const_name NibbleC}, @{const_name NibbleD},
       
    37     @{const_name NibbleE}, @{const_name NibbleF}];
       
    38 in
       
    39   fold (fn target => Code_Target.add_literal_char target charr nibbles)
       
    40     ["SML", "OCaml", "Haskell"]
       
    41   #> Code_Target.add_literal_list_string "Haskell"
       
    42     @{const_name Nil} @{const_name Cons} charr nibbles
       
    43 end
       
    44 *}
    30 *}
    45 
    31 
    46 code_instance char :: eq
    32 code_instance char :: eq
    47   (Haskell -)
    33   (Haskell -)
    48 
    34