src/HOL/Library/Quotient_Set.thy
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 blanchet 2014-03-06 renamed 'vset_rel' to 'rel_vset'
2013-08-13 kuncar 2013-08-13 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
2013-06-10 huffman 2013-06-10 more transfer rules for sets
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-14 huffman 2012-05-14 add transfer rule for set_rel
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 add transfer rule for set difference
2012-04-22 huffman 2012-04-22 new example theory for quotient/transfer
2012-04-21 huffman 2012-04-21 move alternative definition lemmas into Lifting.thy; simplify proof of Quotient_compose
2012-04-21 huffman 2012-04-21 added covariant relator set_rel, with transfer rules for set operations
2012-04-21 huffman 2012-04-21 renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
2012-04-20 huffman 2012-04-20 move definition of set_rel into Library/Quotient_Set.thy
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-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-09-10 krauss 2011-09-10 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
2011-08-24 Cezary Kaliszyk 2011-08-24 Quotient Package: add mem_rsp, mem_prs, tune proofs.
2011-08-23 Cezary Kaliszyk 2011-08-23 Quotient Package: some infrastructure for lifting inside sets