src/HOL/Orderings.thy
changeset 46882 6242b4bc05bc
parent 46691 72d81e789106
child 46884 154dc6ec0041
     1.1 --- a/src/HOL/Orderings.thy	Sun Mar 11 22:06:13 2012 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Mon Mar 12 15:11:24 2012 +0100
     1.3 @@ -1299,7 +1299,7 @@
     1.4  definition
     1.5    "\<bottom> = (\<lambda>x. \<bottom>)"
     1.6  
     1.7 -lemma bot_apply (* CANDIDATE [simp, code] *):
     1.8 +lemma bot_apply [simp] (* CANDIDATE [code] *):
     1.9    "\<bottom> x = \<bottom>"
    1.10    by (simp add: bot_fun_def)
    1.11  
    1.12 @@ -1315,7 +1315,7 @@
    1.13    [no_atp]: "\<top> = (\<lambda>x. \<top>)"
    1.14  declare top_fun_def_raw [no_atp]
    1.15  
    1.16 -lemma top_apply (* CANDIDATE [simp, code] *):
    1.17 +lemma top_apply [simp] (* CANDIDATE [code] *):
    1.18    "\<top> x = \<top>"
    1.19    by (simp add: top_fun_def)
    1.20