src/HOL/Datatype.thy
changeset 19202 0b9eb4b0ad98
parent 19179 61ef97e3f531
child 19347 e2e709f3f955
     1.1 --- a/src/HOL/Datatype.thy	Tue Mar 07 04:06:02 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Tue Mar 07 14:09:48 2006 +0100
     1.3 @@ -246,6 +246,9 @@
     1.4    fst_conv [code]
     1.5    snd_conv [code]
     1.6  
     1.7 +lemma [code unfold]:
     1.8 +  "1 == Suc 0" by simp
     1.9 +
    1.10  code_generate True False Not "op &" "op |" If
    1.11  
    1.12  code_syntax_tyco bool
    1.13 @@ -311,9 +314,4 @@
    1.14      ml (target_atom "SOME")
    1.15      haskell (target_atom "Just")
    1.16  
    1.17 -code_syntax_const
    1.18 -  "1 :: nat"
    1.19 -    ml ("{*Suc 0*}")
    1.20 -    haskell ("{*Suc 0*}")
    1.21 -
    1.22  end