src/HOL/Predicate.thy
2014-09-16 blanchet 2014-09-16 added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-14 blanchet 2014-09-14 disable datatype 'plugins' for internal types
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-05-04 blanchet 2014-05-04 renamed 'xxx_size' to 'size_xxx' for old datatype package
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-02-14 blanchet 2014-02-14 renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2014-02-12 blanchet 2014-02-12 adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'
2013-09-27 Andreas Lochbihler 2013-09-27 prefer Code.abort over code_abort
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
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