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