src/HOL/Datatype.thy
changeset 20453 855f07fabd76
parent 20105 454f4be984b7
child 20523 36a59e5d0039
     1.1 --- a/src/HOL/Datatype.thy	Thu Aug 31 23:01:16 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Fri Sep 01 08:36:51 2006 +0200
     1.3 @@ -261,61 +261,40 @@
     1.4    "split = prod_case"
     1.5  by (simp add: expand_fun_eq split_def prod.cases)
     1.6  
     1.7 -code_typapp bool
     1.8 -  ml (target_atom "bool")
     1.9 -  haskell (target_atom "Bool")
    1.10 +code_type bool
    1.11 +  (SML target_atom "bool")
    1.12 +  (Haskell target_atom "Bool")
    1.13  
    1.14 -code_constapp
    1.15 -  True
    1.16 -    ml (target_atom "true")
    1.17 -    haskell (target_atom "True")
    1.18 -  False
    1.19 -    ml (target_atom "false")
    1.20 -    haskell (target_atom "False")
    1.21 -  Not
    1.22 -    ml (target_atom "not")
    1.23 -    haskell (target_atom "not")
    1.24 -  "op &"
    1.25 -    ml (infixl 1 "andalso")
    1.26 -    haskell (infixl 3 "&&")
    1.27 -  "op |"
    1.28 -    ml (infixl 0 "orelse")
    1.29 -    haskell (infixl 2 "||")
    1.30 -  If
    1.31 -    ml (target_atom "(if __/ then __/ else __)")
    1.32 -    haskell (target_atom "(if __/ then __/ else __)")
    1.33 +code_const True and False and Not and "op &" and "op |" and If
    1.34 +  (SML target_atom "true" and target_atom "false" and target_atom "not"
    1.35 +    and infixl 1 "andalso" and infixl 0 "orelse"
    1.36 +    and target_atom "(if __/ then __/ else __)")
    1.37 +  (Haskell target_atom "True" and target_atom "False" and target_atom "not"
    1.38 +    and infixl 3 "&&" and infixl 2 "||"
    1.39 +    and target_atom "(if __/ then __/ else __)")
    1.40 +
    1.41 +code_type *
    1.42 +  (SML infix 2 "*")
    1.43 +  (Haskell target_atom "(__,/ __)")
    1.44  
    1.45 -code_typapp
    1.46 -  *
    1.47 -    ml (infix 2 "*")
    1.48 -    haskell (target_atom "(__,/ __)")
    1.49 +code_const Pair
    1.50 +  (SML target_atom "(__,/ __)")
    1.51 +  (Haskell target_atom "(__,/ __)")
    1.52  
    1.53 -code_constapp
    1.54 -  Pair
    1.55 -    ml (target_atom "(__,/ __)")
    1.56 -    haskell (target_atom "(__,/ __)")
    1.57 -
    1.58 -code_typapp
    1.59 -  unit
    1.60 -    ml (target_atom "unit")
    1.61 -    haskell (target_atom "()")
    1.62 +code_type unit
    1.63 +  (SML target_atom "unit")
    1.64 +  (Haskell target_atom "()")
    1.65  
    1.66 -code_constapp
    1.67 -  Unity
    1.68 -    ml (target_atom "()")
    1.69 -    haskell (target_atom "()")
    1.70 +code_const Unity
    1.71 +  (SML target_atom "()")
    1.72 +  (Haskell target_atom "()")
    1.73  
    1.74 -code_typapp
    1.75 -  option
    1.76 -    ml ("_ option")
    1.77 -    haskell ("Maybe _")
    1.78 +code_type option
    1.79 +  (SML "_ option")
    1.80 +  (Haskell "Maybe _")
    1.81  
    1.82 -code_constapp
    1.83 -  None
    1.84 -    ml (target_atom "NONE")
    1.85 -    haskell (target_atom "Nothing")
    1.86 -  Some
    1.87 -    ml (target_atom "SOME")
    1.88 -    haskell (target_atom "Just")
    1.89 +code_const None and Some
    1.90 +  (SML target_atom "NONE" and target_atom "SOME")
    1.91 +  (Haskell target_atom "Nothing" and target_atom "Just")
    1.92  
    1.93  end