--- a/src/HOL/Finite_Set.thy Fri Mar 16 21:32:06 2007 +0100
+++ b/src/HOL/Finite_Set.thy Fri Mar 16 21:32:07 2007 +0100
@@ -1979,6 +1979,7 @@
subsubsection{* Semi-Lattices *}
+(*FIXME integrate with Orderings.thy/OrderedGroup.thy*)
locale ACIfSL = ACIf +
fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
and strict_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
@@ -2167,6 +2168,7 @@
subsubsection{* Lattices *}
+(*FIXME integrate with FixedPoint.thy*)
locale Lattice = lattice +
fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)