| 2011-07-07 | Christian Urban | code refactoring; introduced a record for raw_dt_info | file | diff | annotate |
| 2011-06-23 | Christian Urban | fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package | file | diff | annotate |
| 2011-04-13 | Christian Urban | introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive | file | diff | annotate |
| 2010-12-28 | Christian Urban | automated all strong induction lemmas | file | diff | annotate |
| 2010-12-21 | Christian Urban | all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code | file | diff | annotate |
| 2010-12-16 | Christian Urban | simple cases for strong inducts done; infrastructure for the difficult ones is there | file | diff | annotate |
| 2010-12-12 | Christian Urban | created strong_exhausts terms | file | diff | annotate |