--- a/src/HOL/Lattices.thy Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Lattices.thy Sun Feb 26 20:10:14 2012 +0100
@@ -43,13 +43,7 @@
end
-subsection {* Concrete lattices *}
-
-notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- bot ("\<bottom>") and
- top ("\<top>")
+subsection {* Syntactic infimum and supremum operations *}
class inf =
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -57,6 +51,13 @@
class sup =
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+
+subsection {* Concrete lattices *}
+
+notation
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50)
+
class semilattice_inf = order + inf +
assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
@@ -759,12 +760,8 @@
no_notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- top ("\<top>") and
- bot ("\<bottom>")
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50)
end