src/HOL/Quotient_Examples/DList.thy
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-03-23 kuncar 2012-03-23 fix Quotient_Examples
2011-12-26 haftmann 2011-12-26 incorporated More_Set and More_List into the Main body -- to be consolidated later
2011-10-12 wenzelm 2011-10-12 tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-08-18 Cezary Kaliszyk 2011-08-18 Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.
2011-07-12 Cezary Kaliszyk 2011-07-12 Quotient example: Lists with distinct elements