src/HOL/Lattices.thy
 changeset 28562 4e74209f113e parent 27682 25aceefd4786 child 28685 275122631271
```     1.1 --- a/src/HOL/Lattices.thy	Fri Oct 10 06:45:50 2008 +0200
1.2 +++ b/src/HOL/Lattices.thy	Fri Oct 10 06:45:53 2008 +0200
1.3 @@ -9,7 +9,7 @@
1.4  imports Fun
1.5  begin
1.6
1.7 -subsection{* Lattices *}
1.8 +subsection {* Lattices *}
1.9
1.10  notation
1.11    less_eq  (infix "\<sqsubseteq>" 50) and
1.12 @@ -40,7 +40,7 @@
1.13  class lattice = lower_semilattice + upper_semilattice
1.14
1.15
1.16 -subsubsection{* Intro and elim rules*}
1.17 +subsubsection {* Intro and elim rules*}
1.18
1.19  context lower_semilattice
1.20  begin
1.21 @@ -512,10 +512,10 @@
1.22  begin
1.23
1.24  definition
1.25 -  inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
1.26 +  inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
1.27
1.28  definition
1.29 -  sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
1.30 +  sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
1.31
1.32  instance
1.33  apply intro_classes
1.34 @@ -536,10 +536,10 @@
1.35  begin
1.36
1.37  definition
1.38 -  Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
1.39 +  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
1.40
1.41  definition
1.42 -  Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
1.43 +  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
1.44
1.45  instance
1.46    by intro_classes
```