src/HOL/Datatype.thy
changeset 21126 4dbc3ccbaab0
parent 21111 624ed9c7c4fe
child 21243 afffe1f72143
equal deleted inserted replaced
21125:9b7d35ca1eef 21126:4dbc3ccbaab0
   771   (Haskell "Bool")
   771   (Haskell "Bool")
   772 
   772 
   773 code_const True and False and Not and "op &" and "op |" and If
   773 code_const True and False and Not and "op &" and "op |" and If
   774   (SML "true" and "false" and "not"
   774   (SML "true" and "false" and "not"
   775     and infixl 1 "andalso" and infixl 0 "orelse"
   775     and infixl 1 "andalso" and infixl 0 "orelse"
   776     and "!(if __/ then __/ else __)")
   776     and "!(if (_)/ then (_)/ else (_))")
   777   (Haskell "True" and "False" and "not"
   777   (Haskell "True" and "False" and "not"
   778     and infixl 3 "&&" and infixl 2 "||"
   778     and infixl 3 "&&" and infixl 2 "||"
   779     and "!(if __/ then __/ else __)")
   779     and "!(if (_)/ then (_)/ else (_))")
   780 
   780 
   781 code_type *
   781 code_type *
   782   (SML infix 2 "*")
   782   (SML infix 2 "*")
   783   (Haskell "!(__,/ __)")
   783   (Haskell "!((_),/ (_))")
   784 
   784 
   785 code_const Pair
   785 code_const Pair
   786   (SML "!(__,/ __)")
   786   (SML "!((_),/ (_))")
   787   (Haskell "!(__,/ __)")
   787   (Haskell "!((_),/ (_))")
   788 
   788 
   789 code_type unit
   789 code_type unit
   790   (SML "unit")
   790   (SML "unit")
   791   (Haskell "()")
   791   (Haskell "()")
   792 
   792