# HG changeset patch
# User haftmann
# Date 1349866344 -7200
# Node ID c7c2152322f2b9fcb20f820ae113b10873106291
# Parent  3ecfba7e731dd64067707dee0a1aa823c9e981a3
more explicit code equations

diff -r 3ecfba7e731d -r c7c2152322f2 src/HOL/Lattices.thy
--- 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)
 
diff -r 3ecfba7e731d -r c7c2152322f2 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Oct 10 10:48:55 2012 +0200
+++ b/src/HOL/Orderings.thy	Wed Oct 10 12:52:24 2012 +0200
@@ -1296,7 +1296,7 @@
 definition
   "\<bottom> = (\<lambda>x. \<bottom>)"
 
-lemma bot_apply [simp] (* CANDIDATE [code] *):
+lemma bot_apply [simp, code]:
   "\<bottom> x = \<bottom>"
   by (simp add: bot_fun_def)
 
@@ -1311,7 +1311,7 @@
 definition
   [no_atp]: "\<top> = (\<lambda>x. \<top>)"
 
-lemma top_apply [simp] (* CANDIDATE [code] *):
+lemma top_apply [simp, code]:
   "\<top> x = \<top>"
   by (simp add: top_fun_def)