src/HOL/Quotient_Examples/DList.thy
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