--- a/src/HOL/Orderings.thy Sat Feb 25 15:33:36 2012 +0100
+++ b/src/HOL/Orderings.thy Sun Feb 26 15:28:48 2012 +0100
@@ -1299,7 +1299,7 @@
definition
"\<bottom> = (\<lambda>x. \<bottom>)"
-lemma bot_apply:
+lemma bot_apply (* CANDIDATE [simp, code] *):
"\<bottom> x = \<bottom>"
by (simp add: bot_fun_def)
@@ -1315,7 +1315,7 @@
[no_atp]: "\<top> = (\<lambda>x. \<top>)"
declare top_fun_def_raw [no_atp]
-lemma top_apply:
+lemma top_apply (* CANDIDATE [simp, code] *):
"\<top> x = \<top>"
by (simp add: top_fun_def)