--- 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 "\<sqsubseteq>" 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 \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+ inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
definition
- sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+ sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
instance
apply intro_classes
@@ -536,10 +536,10 @@
begin
definition
- Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+ Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
definition
- Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+ Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
instance
by intro_classes