src/HOL/Library/Quotient_Type.thy
2014-12-28 wenzelm 2014-12-28 modernized historic example;
2014-11-02 wenzelm 2014-11-02 modernized header;
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2010-02-10 wenzelm 2010-02-10 renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;