src/HOL/Predicate.thy
2012-04-06 haftmann 2012-04-06 abandoned almost redundant *_foldr lemmas
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-23 haftmann 2012-02-23 moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
2012-02-21 haftmann 2012-02-21 reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-19 haftmann 2012-02-19 distributed lattice properties of predicates to places of instantiation
2012-01-12 berghofe 2012-01-12 Added inf_Int_eq to pred_set_conv database as well
2012-01-10 berghofe 2012-01-10 Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules
2011-12-29 haftmann 2011-12-29 conversions from sets to predicates and vice versa; extensionality on predicates
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-11-25 wenzelm 2011-11-25 proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-08-23 haftmann 2011-08-23 tuned specifications, syntax and proofs
2011-08-22 haftmann 2011-08-22 tuned specifications and syntax
2011-08-21 haftmann 2011-08-21 avoid pred/set mixture
2011-08-04 haftmann 2011-08-04 more fine-granular instantiation
2011-08-03 haftmann 2011-08-03 more specific instantiation
2011-07-29 haftmann 2011-07-29 tuned proofs
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-12-20 haftmann 2010-12-20 type_lifting for predicates
2010-12-08 haftmann 2010-12-08 bot comes before top, inf before sup etc.
2010-12-08 haftmann 2010-12-08 nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
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)