src/HOL/Lattices.thy
changeset 49769 c7c2152322f2
parent 46884 154dc6ec0041
child 50615 965d4c108584
     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