src/HOL/Code_Setup.thy
changeset 28562 4e74209f113e
parent 28537 1e84256d1a8a
child 28687 150a8a1eae1a
     1.1 --- a/src/HOL/Code_Setup.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -21,32 +21,32 @@
     1.4  
     1.5  text {* Code equations *}
     1.6  
     1.7 -lemma [code func]:
     1.8 +lemma [code]:
     1.9    shows "False \<and> x \<longleftrightarrow> False"
    1.10      and "True \<and> x \<longleftrightarrow> x"
    1.11      and "x \<and> False \<longleftrightarrow> False"
    1.12      and "x \<and> True \<longleftrightarrow> x" by simp_all
    1.13  
    1.14 -lemma [code func]:
    1.15 +lemma [code]:
    1.16    shows "False \<or> x \<longleftrightarrow> x"
    1.17      and "True \<or> x \<longleftrightarrow> True"
    1.18      and "x \<or> False \<longleftrightarrow> x"
    1.19      and "x \<or> True \<longleftrightarrow> True" by simp_all
    1.20  
    1.21 -lemma [code func]:
    1.22 +lemma [code]:
    1.23    shows "\<not> True \<longleftrightarrow> False"
    1.24      and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
    1.25  
    1.26 -lemmas [code func] = Let_def if_True if_False
    1.27 +lemmas [code] = Let_def if_True if_False
    1.28  
    1.29 -lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
    1.30 +lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
    1.31  
    1.32  text {* Equality *}
    1.33  
    1.34  context eq
    1.35  begin
    1.36  
    1.37 -lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
    1.38 +lemma equals_eq [code inline, code]: "op = \<equiv> eq"
    1.39    by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    1.40  
    1.41  declare eq [code unfold, code inline del]