--- a/src/HOL/Lattices.thy Wed Oct 10 10:48:55 2012 +0200
+++ b/src/HOL/Lattices.thy Wed Oct 10 12:52:24 2012 +0200
@@ -650,14 +650,14 @@
definition
"f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
-lemma inf_apply [simp] (* CANDIDATE [code] *):
+lemma inf_apply [simp, code]:
"(f \<sqinter> g) x = f x \<sqinter> g x"
by (simp add: inf_fun_def)
definition
"f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
-lemma sup_apply [simp] (* CANDIDATE [code] *):
+lemma sup_apply [simp, code]:
"(f \<squnion> g) x = f x \<squnion> g x"
by (simp add: sup_fun_def)
@@ -677,7 +677,7 @@
definition
fun_Compl_def: "- A = (\<lambda>x. - A x)"
-lemma uminus_apply [simp] (* CANDIDATE [code] *):
+lemma uminus_apply [simp, code]:
"(- A) x = - (A x)"
by (simp add: fun_Compl_def)
@@ -691,7 +691,7 @@
definition
fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
-lemma minus_apply [simp] (* CANDIDATE [code] *):
+lemma minus_apply [simp, code]:
"(A - B) x = A x - B x"
by (simp add: fun_diff_def)