| Mon, 26 Dec 2011 22:17:10 +0100 | haftmann | incorporated More_Set and More_List into the Main body -- to be consolidated later | file | diff | annotate |
| Wed, 12 Oct 2011 20:16:48 +0200 | wenzelm | tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations; | file | diff | annotate |
| 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. | file | diff | annotate |
| Tue, 12 Jul 2011 16:00:05 +0900 | Cezary Kaliszyk | Quotient example: Lists with distinct elements | file | diff | annotate |