| 2011-01-06 | Christian Urban | removed debugging code abd introduced a guarded tracing function | file | diff | annotate |
| 2011-01-06 | Christian Urban | cleaned up weakening proof and added a version with finit sets | file | diff | annotate |
| 2011-01-06 | Christian Urban | made sure the raw datatypes and raw functions do not get any mixfix syntax | file | diff | annotate |
| 2011-01-05 | Christian Urban | exported the code into a separate file | file | diff | annotate |
| 2010-12-31 | Christian Urban | changed res keyword to set+ for restrictions; comment by a referee | file | diff | annotate |
| 2010-12-31 | Christian Urban | added proper case names for all induct and exhaust theorems | file | diff | annotate |
| 2010-12-30 | Christian Urban | removed local fix for bug in induction_schema; added setup method for strong inductions | file | diff | annotate |
| 2010-12-28 | Christian Urban | automated all strong induction lemmas | file | diff | annotate |