Nominal/nominal_inductive.ML
Thu, 09 Jul 2015 02:32:46 +0100 Christian Urban updated for Isabelle 2015
Mon, 24 Mar 2014 15:31:17 +0000 Christian Urban updated to massive changes in Isabelle
Fri, 19 Apr 2013 00:10:52 +0100 Christian Urban updated to simplifier changes
Wed, 27 Mar 2013 16:08:30 +0100 webertj Various changes to support Nominal2 commands in local contexts.
Mon, 18 Jun 2012 14:50:02 +0100 Christian Urban used ML-antiquotation command_spec for new commands
Tue, 20 Mar 2012 11:26:10 +0000 Christian Urban updated to new Isabelle (20 March)
Fri, 17 Feb 2012 15:23:38 +0100 Cezary Kaliszyk Update from Isabelle Wed Feb 15 23:19:30
Mon, 16 Jan 2012 12:42:47 +0000 Christian Urban updated to Isabelle 16 January
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
Fri, 19 Aug 2011 10:56:12 +0900 Cezary Kaliszyk Update to new Isabelle
Mon, 15 Aug 2011 10:43:22 +0200 Christian Urban updated for new Isabelle (11. Aug.)
Mon, 18 Apr 2011 15:56:07 +0100 Christian Urban added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April
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
Wed, 19 Jan 2011 17:54:06 +0100 Christian Urban removed diagnostic code
Thu, 06 Jan 2011 14:02:10 +0000 Christian Urban tuned
Wed, 05 Jan 2011 17:33:43 +0000 Christian Urban exported the code into a separate file
less more (0) tip