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
```