src/HOL/Predicate.thy
2010-11-29 haftmann 2010-11-29 moved generic definitions about relations from Quotient.thy to Predicate; more natural deduction rules
2010-11-22 haftmann 2010-11-22 adhere established Collect/mem convention more closely
2010-11-19 haftmann 2010-11-19 eval simp rules for predicate type, simplify primitive proofs
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-23 blanchet 2010-08-23 "no_atp" fact that leads to unsound Sledgehammer proofs
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-24 blanchet 2010-06-24 yields ill-typed ATP/metis proofs -- raus!
2010-04-29 haftmann 2010-04-29 code_reflect: specify module name directly after keyword
2010-04-28 haftmann 2010-04-28 avoid code_datatype antiquotation
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-28 huffman 2010-03-28 add/change some lemmas about lattices
2009-12-11 haftmann 2009-12-11 moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
2009-12-05 haftmann 2009-12-05 tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-12-04 haftmann 2009-12-04 tuned code setup
2009-11-19 bulwahn 2009-11-19 adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
2009-11-12 bulwahn 2009-11-12 removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
2009-11-11 haftmann 2009-11-11 tuned
2009-10-24 bulwahn 2009-10-24 developing an executable the operator
2009-10-24 bulwahn 2009-10-24 generalizing singleton with a default value
2009-10-24 bulwahn 2009-10-24 moved meta_fun_cong lemma into ML-file; tuned
2009-10-06 haftmann 2009-10-06 inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
2009-09-30 haftmann 2009-09-30 moved lemmas about sup on bool to Lattices.thy
2009-09-30 haftmann 2009-09-30 tuned headings
2009-09-25 haftmann 2009-09-25 merged
2009-09-23 haftmann 2009-09-23 removed potentially dangerous rules from pred_set_conv
2009-09-23 bulwahn 2009-09-23 added first prototype of the extended predicate compiler
2009-09-18 haftmann 2009-09-18 be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
2009-09-15 haftmann 2009-09-15 hide new constants
2009-09-15 haftmann 2009-09-15 added emptiness check predicate and singleton projection
2009-08-14 haftmann 2009-08-14 formally stylized
2009-07-27 krauss 2009-07-27 "more standard" argument order of relation composition (op O)
2009-07-03 haftmann 2009-07-03 avoid useless code equations
2009-05-21 haftmann 2009-05-21 added Predicate.map in SML environment
2009-05-20 haftmann 2009-05-20 added Predicate.map
2009-05-13 haftmann 2009-05-13 dropped sort constraint on predicate equality
2009-05-12 haftmann 2009-05-12 added dummy values keyword
2009-05-11 haftmann 2009-05-11 avoid latex output problem
2009-05-11 haftmann 2009-05-11 merged
2009-05-11 bulwahn 2009-05-11 Added pred_code command
2009-04-22 bulwahn 2009-04-22 added general preprocessing of equality in predicates for code generation
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.