--- a/src/HOL/Lattices.thy Sat Nov 10 18:36:10 2007 +0100
+++ b/src/HOL/Lattices.thy Sat Nov 10 23:03:52 2007 +0100
@@ -12,9 +12,8 @@
subsection{* Lattices *}
notation
- less_eq (infix "\<sqsubseteq>" 50)
-and
- less (infix "\<sqsubset>" 50)
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50)
class lower_semilattice = order +
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -30,6 +29,7 @@
class lattice = lower_semilattice + upper_semilattice
+
subsubsection{* Intro and elim rules*}
context lower_semilattice
@@ -398,13 +398,11 @@
by (simp add: Sup_insert_simp)
definition
- top :: 'a
-where
+ top :: 'a where
"top = \<Sqinter>{}"
definition
- bot :: 'a
-where
+ bot :: 'a where
"bot = \<Squnion>{}"
lemma top_greatest [simp]: "x \<le> top"
@@ -586,16 +584,11 @@
lemmas sup_aci = sup_ACI
no_notation
- less_eq (infix "\<sqsubseteq>" 50)
-and
- less (infix "\<sqsubset>" 50)
-and
- inf (infixl "\<sqinter>" 70)
-and
- sup (infixl "\<squnion>" 65)
-and
- Inf ("\<Sqinter>_" [900] 900)
-and
- Sup ("\<Squnion>_" [900] 900)
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50) and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65) and
+ Inf ("\<Sqinter>_" [900] 900) and
+ Sup ("\<Squnion>_" [900] 900)
end