src/HOL/Finite_Set.thy

   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
   -- {* No more proofs involve these relations. *}
 
 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)
   assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
   defines strict_below_def:  "(x \<sqsubset> y) \<equiv> (x \<sqsubseteq> y \<and> x \<noteq> y)"

 
 
 
 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)
   defines "Inf == fold1 inf"  and "Sup == fold1 sup"