src/HOL/Library/Code_Char.thy
changeset 31053 b7e1c065b6e4
parent 31046 c1969f609bf7
child 32657 5f13912245ff
equal deleted inserted replaced
31052:9a3bd9dbdd0f 31053:b7e1c065b6e4
    12   (SML "char")
    12   (SML "char")
    13   (OCaml "char")
    13   (OCaml "char")
    14   (Haskell "Char")
    14   (Haskell "Char")
    15 
    15 
    16 setup {*
    16 setup {*
    17   fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] 
    17   fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] 
    18   #> add_literal_list_string "Haskell"
    18   #> String_Code.add_literal_list_string "Haskell"
    19 *}
    19 *}
    20 
    20 
    21 code_instance char :: eq
    21 code_instance char :: eq
    22   (Haskell -)
    22   (Haskell -)
    23 
    23