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