| 2011-01-06 | Christian Urban | a modified function package where, as a test, True has been injected into the compatibility condictions | file | diff | annotate |
| 2011-01-06 | Christian Urban | tuned | file | diff | annotate |
| 2010-12-31 | Christian Urban | changed res keyword to set+ for restrictions; comment by a referee | file | diff | annotate |
| 2010-12-28 | Christian Urban | automated all strong induction lemmas | file | diff | annotate |
| 2010-12-22 | Christian Urban | properly exported strong exhaust theorem; cleaned up some examples | file | diff | annotate |
| 2010-11-10 | Christian Urban | adapted to changes by Florian on the quotient package and removed local fix for function package | file | diff | annotate |
| 2010-09-29 | Christian Urban | simplified exhaust proofs | file | diff | annotate |