20080507 
berghofe 
20080507 
 Added mem_def and predicate1I in some of the proofs
 pred_equals_eq and pred_subset_eq are no longer used in the conversion
between sets and predicates, because sets and predicates can no longer
be distinguished

file  diff  annotate 
20070820 
haftmann 
20070820 
Sup now explicit parameter of complete_lattice

file  diff  annotate 
20070711 
berghofe 
20070711 
 Moved infrastructure for converting between sets and predicates
to Tools/inductive_set_package.ML
 Adapted conversion rules to new format (now use standard op :
and Collect operators rather than Collect2 and member(2))
 Removed bounded quantifiers for predicates

file  diff  annotate 
20070710 
haftmann 
20070710 
clarified import

file  diff  annotate 
20070614 
wenzelm 
20070614 
tuned proofs: avoid implicit prems;

file  diff  annotate 
20070507 
wenzelm 
20070507 
simplified DataFun interfaces;

file  diff  annotate 
20070310 
berghofe 
20070310 
Generalized version of SUP and INF (with index set).

file  diff  annotate 
20070309 
haftmann 
20070309 
stepping towards uniform lattice theory development in HOL

file  diff  annotate 
20070207 
berghofe 
20070207 
New theory for converting between predicates and sets.

file  diff  annotate 