Tue, 06 Dec 2011 23:42:19 +0000 | Christian Urban | updated to Isabelle 6 Dec (thanks to Odrej Kuncar) | file | diff | annotate |
Thu, 03 Nov 2011 13:19:23 +0000 | Christian Urban | updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package | file | diff | annotate |
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 |