src/HOL/Predicate.thy
2009-04-22 haftmann 2009-04-22 fixed compilation of predicate types in ML environment
2009-04-17 haftmann 2009-04-17 static compilation of enumeration type
2009-03-11 haftmann 2009-03-11 explicit code equations for some rarely used pred operations
2009-03-09 haftmann 2009-03-09 dropped eq_pred
2009-03-08 haftmann 2009-03-08 refined enumeration implementation
2009-03-06 haftmann 2009-03-06 added enumeration of predicates
2008-05-07 berghofe 2008-05-07 - 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
2007-08-20 haftmann 2007-08-20 Sup now explicit parameter of complete_lattice
2007-07-11 berghofe 2007-07-11 - 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
2007-07-10 haftmann 2007-07-10 clarified import
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-03-10 berghofe 2007-03-10 Generalized version of SUP and INF (with index set).
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-02-07 berghofe 2007-02-07 New theory for converting between predicates and sets.