src/HOL/Quotient_Examples/DList.thy
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit
Fri, 23 Mar 2012 14:17:29 +0100 kuncar fix Quotient_Examples
Mon, 26 Dec 2011 22:17:10 +0100 haftmann incorporated More_Set and More_List into the Main body -- to be consolidated later
Wed, 12 Oct 2011 20:16:48 +0200 wenzelm tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
Thu, 18 Aug 2011 16:52:19 +0900 Cezary Kaliszyk Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.
Tue, 12 Jul 2011 16:00:05 +0900 Cezary Kaliszyk Quotient example: Lists with distinct elements
less more (0) tip