diff -r 056255ade52a -r 4e74209f113e src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Fri Oct 10 06:45:50 2008 +0200 +++ b/src/HOL/Lattices.thy Fri Oct 10 06:45:53 2008 +0200 @@ -9,7 +9,7 @@ imports Fun begin -subsection{* Lattices *} +subsection {* Lattices *} notation less_eq (infix "\" 50) and @@ -40,7 +40,7 @@ class lattice = lower_semilattice + upper_semilattice -subsubsection{* Intro and elim rules*} +subsubsection {* Intro and elim rules*} context lower_semilattice begin @@ -512,10 +512,10 @@ begin definition - inf_fun_eq [code func del]: "f \ g = (\x. f x \ g x)" + inf_fun_eq [code del]: "f \ g = (\x. f x \ g x)" definition - sup_fun_eq [code func del]: "f \ g = (\x. f x \ g x)" + sup_fun_eq [code del]: "f \ g = (\x. f x \ g x)" instance apply intro_classes @@ -536,10 +536,10 @@ begin definition - Inf_fun_def [code func del]: "\A = (\x. \{y. \f\A. y = f x})" + Inf_fun_def [code del]: "\A = (\x. \{y. \f\A. y = f x})" definition - Sup_fun_def [code func del]: "\A = (\x. \{y. \f\A. y = f x})" + Sup_fun_def [code del]: "\A = (\x. \{y. \f\A. y = f x})" instance by intro_classes