src/HOL/Library/Quotient_Option.thy
2016-04-11 wenzelm 2016-04-11 tuned imports;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-04-10 kuncar 2014-04-10 simplify and fix theories thanks to 356a5efdb278
2014-02-18 kuncar 2014-02-18 delete or move now not necessary reflexivity rules due to 1726f46d2aa8
2014-02-16 blanchet 2014-02-16 folded 'rel_option' into 'option_rel'
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2013-08-13 traytel 2013-08-13 got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
2013-08-13 kuncar 2013-08-13 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
2013-08-13 kuncar 2013-08-13 move useful lemmas to Main
2013-05-15 kuncar 2013-05-15 stronger reflexivity prover
2013-05-13 kuncar 2013-05-13 better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
2013-03-08 kuncar 2013-03-08 add [relator_mono] and [relator_distr] rules
2012-05-24 kuncar 2012-05-24 prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
2012-05-16 kuncar 2012-05-16 infrastructure that makes possible to prove that a relation is reflexive
2012-04-26 kuncar 2012-04-26 use a quot_map theorem attribute instead of the complicated map attribute
2012-04-20 huffman 2012-04-20 rename 'correspondence' method to 'transfer_prover'
2012-04-20 kuncar 2012-04-20 hide the invariant constant for relators: invariant_commute infrastracture
2012-04-20 huffman 2012-04-20 add new transfer rules and setup for lifting package
2012-04-13 wenzelm 2012-04-13 updated headers;
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-03-23 kuncar 2012-03-23 store the relational theorem for every relator
2011-12-09 kuncar 2011-12-09 Quotient_Info stores only relation maps
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-11-30 haftmann 2010-11-30 more systematic and compact proofs on type relation operators using natural deduction rules
2010-11-15 haftmann 2010-11-15 re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
2010-11-09 haftmann 2010-11-09 type annotations in specifications; fun_rel_def is no simp rule by default
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-03-14 wenzelm 2010-03-14 observe standard header format;
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.