src/HOL/Datatype.thy
changeset 20523 36a59e5d0039
parent 20453 855f07fabd76
child 20588 c847c56edf0c
     1.1 --- a/src/HOL/Datatype.thy	Wed Sep 13 00:38:38 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Sep 13 12:05:50 2006 +0200
     1.3 @@ -233,27 +233,27 @@
     1.4  
     1.5  lemmas [code] = imp_conv_disj
     1.6  
     1.7 -lemma [code fun]:
     1.8 +lemma [code func]:
     1.9    "(\<not> True) = False" by (rule HOL.simp_thms)
    1.10  
    1.11 -lemma [code fun]:
    1.12 +lemma [code func]:
    1.13    "(\<not> False) = True" by (rule HOL.simp_thms)
    1.14  
    1.15 -lemma [code fun]:
    1.16 +lemma [code func]:
    1.17    shows "(False \<and> x) = False"
    1.18    and   "(True \<and> x) = x"
    1.19    and   "(x \<and> False) = False"
    1.20    and   "(x \<and> True) = x" by simp_all
    1.21  
    1.22 -lemma [code fun]:
    1.23 +lemma [code func]:
    1.24    shows "(False \<or> x) = x"
    1.25    and   "(True \<or> x) = True"
    1.26    and   "(x \<or> False) = x"
    1.27    and   "(x \<or> True) = True" by simp_all
    1.28  
    1.29  declare
    1.30 -  if_True [code fun]
    1.31 -  if_False [code fun]
    1.32 +  if_True [code func]
    1.33 +  if_False [code func]
    1.34    fst_conv [code]
    1.35    snd_conv [code]
    1.36