src/HOL/Predicate.thy
2018-03-26 Manuel Eberl Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
2018-03-12 Manuel Eberl Changes to complete distributive lattices due to Viorel Preoteasa
2018-01-10 nipkow ran isabelle update_op on all sources
2017-11-26 wenzelm more symbols;
2017-07-02 haftmann proper concept of code declaration wrt. atomicity and Isar declarations
2017-06-05 haftmann modernized (code) setup for enumeration predicates
2016-02-23 nipkow more canonical names
2016-01-01 wenzelm more symbols;
2015-07-18 wenzelm isabelle update_cartouches;
2015-05-01 wenzelm tuned spelling;
2014-11-02 wenzelm modernized header uniformly as section;
2014-09-16 blanchet added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-14 blanchet disable datatype 'plugins' for internal types
2014-09-11 blanchet updated news
2014-09-02 blanchet use 'datatype_new' in 'Main'
2014-05-04 blanchet renamed 'xxx_size' to 'size_xxx' for old datatype package
2014-03-19 haftmann 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 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-16 haftmann normalising simp rules for compound operators
2014-03-15 haftmann more complete set of lemmas wrt. image and composition
2014-02-14 blanchet renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2014-02-12 blanchet adapted theories to 'xxx_case' to 'case_xxx'
2013-09-27 Andreas Lochbihler prefer Code.abort over code_abort
2013-09-02 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
2013-02-15 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
2013-02-14 haftmann reform of predicate compiler / quickcheck theories:
2013-02-14 haftmann abandoned theory Plain
2012-04-06 haftmann abandoned almost redundant *_foldr lemmas
2012-03-12 noschinl tuned proofs
2012-02-24 haftmann 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 given up disfruitful branch
2012-02-24 haftmann 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 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 reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-19 haftmann distributed lattice properties of predicates to places of instantiation
2012-01-11 berghofe Added inf_Int_eq to pred_set_conv database as well
2012-01-10 berghofe Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules
2011-12-29 haftmann conversions from sets to predicates and vice versa; extensionality on predicates
2011-12-24 haftmann adjusted to set/pred distinction by means of type constructor `set`
2011-11-25 wenzelm 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 renamed Complete_Lattices lemmas, removed legacy names
2011-08-23 haftmann tuned specifications, syntax and proofs
2011-08-22 haftmann tuned specifications and syntax
2011-08-21 haftmann avoid pred/set mixture
2011-08-04 haftmann more fine-granular instantiation
2011-08-03 haftmann more specific instantiation
2011-07-29 haftmann tuned proofs
2011-01-14 wenzelm eliminated global prems;
2011-01-11 haftmann "enriched_type" replaces less specific "type_lifting"
2010-12-21 haftmann tuned type_lifting declarations
2010-12-20 haftmann type_lifting for predicates
2010-12-08 haftmann bot comes before top, inf before sup etc.
2010-12-08 haftmann nice syntax for lattice INFI, SUPR;
2010-12-08 haftmann primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-11-29 haftmann moved generic definitions about relations from Quotient.thy to Predicate;
2010-11-22 haftmann adhere established Collect/mem convention more closely
2010-11-19 haftmann eval simp rules for predicate type, simplify primitive proofs
2010-09-13 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow expand_fun_eq -> ext_iff
2010-08-27 haftmann renamed class/constant eq to equal; tuned some instantiations
less more (0) -100 -60 tip