src/HOL/Code_Setup.thy
changeset 27454 fb6a272fe5d0
parent 27103 d8549f4d900b
child 28012 2308843f8b66
equal deleted inserted replaced
27453:eecd9d84e41b 27454:fb6a272fe5d0
    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 func, code unfold, code post] = imp_conv_disj
    89 lemmas [code func, code unfold, symmetric, code post] = 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")