src/HOL/Complete_Lattice.thy
changeset 37767 a2b7a20d6ea3
parent 36635 080b755377c0
child 38705 aaee86c0e237
     1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Jul 12 08:58:27 2010 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Jul 12 10:48:37 2010 +0200
     1.3 @@ -193,10 +193,10 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
     1.8 +  Inf_fun_def: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
     1.9  
    1.10  definition
    1.11 -  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
    1.12 +  Sup_fun_def: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
    1.13  
    1.14  instance proof
    1.15  qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
    1.16 @@ -457,7 +457,7 @@
    1.17  notation (xsymbols)
    1.18    Inter  ("\<Inter>_" [90] 90)
    1.19  
    1.20 -lemma Inter_eq [code del]:
    1.21 +lemma Inter_eq:
    1.22    "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
    1.23  proof (rule set_ext)
    1.24    fix x