src/HOL/Library/Quotient_List.thy
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
2016-08-10 wenzelm 2016-08-10 tuned proofs;
2016-04-11 wenzelm 2016-04-11 tuned imports;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-10 traytel 2014-11-10 dropped redundant transfer rules (now proved and registered by datatype and plugins)
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-02-18 kuncar 2014-02-18 delete or move now not necessary reflexivity rules due to 1726f46d2aa8
2013-08-13 kuncar 2013-08-13 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
2013-06-05 kuncar 2013-06-05 transfer rule for listsum
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-05-15 huffman 2012-05-15 transfer rules for many more list constants
2012-05-14 huffman 2012-05-14 add transfer rule for constant List.lists
2012-04-26 kuncar 2012-04-26 use a quot_map theorem attribute instead of the complicated map attribute
2012-04-22 huffman 2012-04-22 new example theory for quotient/transfer
2012-04-21 huffman 2012-04-21 add transfer rule for List.set
2012-04-21 huffman 2012-04-21 remove duplicate of lemma id_transfer
2012-04-21 huffman 2012-04-21 new transfer package rules and lifting setup for lists
2012-04-20 kuncar 2012-04-20 hide the invariant constant for relators: invariant_commute infrastracture
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
2012-02-24 haftmann 2012-02-24 explicit is better than implicit
2011-12-10 huffman 2011-12-10 merged
2011-12-09 huffman 2011-12-09 remove some duplicate lemmas, simplify some proofs
2011-12-09 kuncar 2011-12-09 Quotient_Info stores only relation maps
2010-11-30 haftmann 2010-11-30 more systematic and compact proofs on type relation operators using natural deduction rules
2010-11-09 haftmann 2010-11-09 fun_rel_def is no simp rule by default
2010-10-19 bulwahn 2010-10-19 removing something that probably slipped into the Quotient_List theory
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-06-23 Cezary Kaliszyk 2010-06-23 Replace 'list_rel' by 'list_all2'; they are equivalent.
2010-05-11 Christian Urban 2010-05-11 tuned proof so that no simplifier warning is printed
2010-04-22 Cezary Kaliszyk 2010-04-22 fun_rel introduction and list_rel elimination for quotient package
2010-04-20 Cezary Kaliszyk 2010-04-20 respectfullness and preservation of map for identity quotients
2010-04-15 Cezary Kaliszyk 2010-04-15 Respectfullness and preservation of list_rel
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.