# HG changeset patch
# User haftmann
# Date 1174077127 -3600
# Node ID 989182f660e0b0f29ab7bf5e7b17938aa4cdbc53
# Parent  51ee032f959190e69d5482b2025332ce483b69b2
added FIXME hints

diff -r 51ee032f9591 -r 989182f660e0 src/HOL/Finite_Set.thy
--- 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)