--- a/src/HOL/Complete_Lattices.thy Sat Feb 25 15:33:36 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy Sun Feb 26 15:28:48 2012 +0100
@@ -582,14 +582,14 @@
definition
"\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
-lemma Inf_apply [code]:
+lemma Inf_apply (* CANDIDATE [simp] *) [code]:
"(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
by (simp add: Inf_fun_def)
definition
"\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
-lemma Sup_apply [code]:
+lemma Sup_apply (* CANDIDATE [simp] *) [code]:
"(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
by (simp add: Sup_fun_def)
@@ -598,11 +598,11 @@
end
-lemma INF_apply:
+lemma INF_apply (* CANDIDATE [simp] *):
"(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
-lemma SUP_apply:
+lemma SUP_apply (* CANDIDATE [simp] *):
"(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)