src/HOL/Datatype.thy
changeset 19890 1aad48bcc674
parent 19817 bb16bf9ae3fd
child 20105 454f4be984b7
     1.1 --- a/src/HOL/Datatype.thy	Wed Jun 14 12:14:13 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Jun 14 12:14:42 2006 +0200
     1.3 @@ -257,14 +257,11 @@
     1.4    fst_conv [code]
     1.5    snd_conv [code]
     1.6  
     1.7 -lemma [code unfolt]:
     1.8 -  "1 == Suc 0" by simp
     1.9 -
    1.10 -code_syntax_tyco bool
    1.11 +code_typapp bool
    1.12    ml (target_atom "bool")
    1.13    haskell (target_atom "Bool")
    1.14  
    1.15 -code_syntax_const
    1.16 +code_constapp
    1.17    True
    1.18      ml (target_atom "true")
    1.19      haskell (target_atom "True")
    1.20 @@ -284,32 +281,32 @@
    1.21      ml (target_atom "(if __/ then __/ else __)")
    1.22      haskell (target_atom "(if __/ then __/ else __)")
    1.23  
    1.24 -code_syntax_tyco
    1.25 +code_typapp
    1.26    *
    1.27      ml (infix 2 "*")
    1.28      haskell (target_atom "(__,/ __)")
    1.29  
    1.30 -code_syntax_const
    1.31 +code_constapp
    1.32    Pair
    1.33      ml (target_atom "(__,/ __)")
    1.34      haskell (target_atom "(__,/ __)")
    1.35  
    1.36 -code_syntax_tyco
    1.37 +code_typapp
    1.38    unit
    1.39      ml (target_atom "unit")
    1.40      haskell (target_atom "()")
    1.41  
    1.42 -code_syntax_const
    1.43 +code_constapp
    1.44    Unity
    1.45      ml (target_atom "()")
    1.46      haskell (target_atom "()")
    1.47  
    1.48 -code_syntax_tyco
    1.49 +code_typapp
    1.50    option
    1.51      ml ("_ option")
    1.52      haskell ("Maybe _")
    1.53  
    1.54 -code_syntax_const
    1.55 +code_constapp
    1.56    None
    1.57      ml (target_atom "NONE")
    1.58      haskell (target_atom "Nothing")