src/HOL/Code_Setup.thy
changeset 25916 d957d9982241
parent 25885 6fbc3f54f819
child 25962 13b6c0b31005
equal deleted inserted replaced
25915:f1bce5261dec 25916:d957d9982241
    84   (Haskell infixl 4 "==")
    84   (Haskell infixl 4 "==")
    85 
    85 
    86 
    86 
    87 text {* type bool *}
    87 text {* type bool *}
    88 
    88 
    89 lemmas [code unfold] = imp_conv_disj
    89 lemmas [code func, code unfold] = imp_conv_disj
    90 
    90 
    91 code_type bool
    91 code_type bool
    92   (SML "bool")
    92   (SML "bool")
    93   (OCaml "bool")
    93   (OCaml "bool")
    94   (Haskell "Bool")
    94   (Haskell "Bool")