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