| Thu, 07 Jul 2011 16:16:42 +0200 | Christian Urban | code refactoring; introduced a record for raw_dt_info | file | diff | annotate |
| Thu, 23 Jun 2011 11:30:39 +0100 | 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 |
| Wed, 13 Apr 2011 13:41:52 +0100 | Christian Urban | introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive | file | diff | annotate |
| Tue, 28 Dec 2010 19:51:25 +0000 | Christian Urban | automated all strong induction lemmas | file | diff | annotate |
| Tue, 21 Dec 2010 10:28:08 +0000 | 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 |
| Thu, 16 Dec 2010 08:42:48 +0000 | Christian Urban | simple cases for strong inducts done; infrastructure for the difficult ones is there | file | diff | annotate |