Nominal/nominal_dt_rawfuns.ML
Tue, 06 Dec 2011 23:42:19 +0000 Christian Urban updated to Isabelle 6 Dec (thanks to Odrej Kuncar)
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
Thu, 07 Jul 2011 16:16:42 +0200 Christian Urban code refactoring; introduced a record for raw_dt_info
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
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
Tue, 28 Dec 2010 19:51:25 +0000 Christian Urban automated all strong induction lemmas
less more (0) -30 -10 -6 tip