src/HOL/Library/Quotient_Set.thy
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