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