src/HOL/Orderings.thy

 begin
 
 definition
   "\<bottom> = (\<lambda>x. \<bottom>)"
 
-lemma bot_apply:
+lemma bot_apply (* CANDIDATE [simp, code] *):
   "\<bottom> x = \<bottom>"
   by (simp add: bot_fun_def)
 
 instance proof
 qed (simp add: le_fun_def bot_apply)

 
 definition
   [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)
 
 instance proof
 qed (simp add: le_fun_def top_apply)