more explicit code equations
authorhaftmann
Wed Oct 10 12:52:24 2012 +0200 (2012-10-10)
changeset 49769c7c2152322f2
parent 49768 3ecfba7e731d
child 49771 b1493798d253
more explicit code equations
src/HOL/Lattices.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Lattices.thy	Wed Oct 10 10:48:55 2012 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Wed Oct 10 12:52:24 2012 +0200
     1.3 @@ -650,14 +650,14 @@
     1.4  definition
     1.5    "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
     1.6  
     1.7 -lemma inf_apply [simp] (* CANDIDATE [code] *):
     1.8 +lemma inf_apply [simp, code]:
     1.9    "(f \<sqinter> g) x = f x \<sqinter> g x"
    1.10    by (simp add: inf_fun_def)
    1.11  
    1.12  definition
    1.13    "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    1.14  
    1.15 -lemma sup_apply [simp] (* CANDIDATE [code] *):
    1.16 +lemma sup_apply [simp, code]:
    1.17    "(f \<squnion> g) x = f x \<squnion> g x"
    1.18    by (simp add: sup_fun_def)
    1.19  
    1.20 @@ -677,7 +677,7 @@
    1.21  definition
    1.22    fun_Compl_def: "- A = (\<lambda>x. - A x)"
    1.23  
    1.24 -lemma uminus_apply [simp] (* CANDIDATE [code] *):
    1.25 +lemma uminus_apply [simp, code]:
    1.26    "(- A) x = - (A x)"
    1.27    by (simp add: fun_Compl_def)
    1.28  
    1.29 @@ -691,7 +691,7 @@
    1.30  definition
    1.31    fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
    1.32  
    1.33 -lemma minus_apply [simp] (* CANDIDATE [code] *):
    1.34 +lemma minus_apply [simp, code]:
    1.35    "(A - B) x = A x - B x"
    1.36    by (simp add: fun_diff_def)
    1.37  
     2.1 --- a/src/HOL/Orderings.thy	Wed Oct 10 10:48:55 2012 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Wed Oct 10 12:52:24 2012 +0200
     2.3 @@ -1296,7 +1296,7 @@
     2.4  definition
     2.5    "\<bottom> = (\<lambda>x. \<bottom>)"
     2.6  
     2.7 -lemma bot_apply [simp] (* CANDIDATE [code] *):
     2.8 +lemma bot_apply [simp, code]:
     2.9    "\<bottom> x = \<bottom>"
    2.10    by (simp add: bot_fun_def)
    2.11  
    2.12 @@ -1311,7 +1311,7 @@
    2.13  definition
    2.14    [no_atp]: "\<top> = (\<lambda>x. \<top>)"
    2.15  
    2.16 -lemma top_apply [simp] (* CANDIDATE [code] *):
    2.17 +lemma top_apply [simp, code]:
    2.18    "\<top> x = \<top>"
    2.19    by (simp add: top_fun_def)
    2.20