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]
```