src/HOL/Finite_Set.thy
changeset 22451 989182f660e0
parent 22425 c252770ae2d0
child 22473 753123c89d72
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Mar 16 21:32:06 2007 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Mar 16 21:32:07 2007 +0100
     1.3 @@ -1979,6 +1979,7 @@
     1.4  
     1.5  subsubsection{* Semi-Lattices *}
     1.6  
     1.7 +(*FIXME integrate with Orderings.thy/OrderedGroup.thy*)
     1.8  locale ACIfSL = ACIf +
     1.9    fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
    1.10    and strict_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
    1.11 @@ -2167,6 +2168,7 @@
    1.12  
    1.13  subsubsection{* Lattices *}
    1.14  
    1.15 +(*FIXME integrate with FixedPoint.thy*)
    1.16  locale Lattice = lattice +
    1.17    fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    1.18    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)