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