| Thu, 19 Apr 2018 13:57:17 +0100 |
Christian Urban |
updated to Isabelle 2016-1
default
|
file |
diff |
annotate
|
| Sat, 19 Mar 2016 21:06:48 +0000 |
Christian Urban |
updated to Isabelle 2016
Nominal2-Isabelle2016
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 02:32:46 +0100 |
Christian Urban |
updated for Isabelle 2015
|
file |
diff |
annotate
|
| Mon, 19 May 2014 16:45:46 +0100 |
Christian Urban |
changed nominal_primrec to nominal_function and termination to nominal_termination
|
file |
diff |
annotate
|
| Mon, 19 May 2014 12:45:26 +0100 |
Christian Urban |
changed nominal_primrec into the more appropriate nominal_function
|
file |
diff |
annotate
|
| Mon, 19 May 2014 11:19:48 +0100 |
Christian Urban |
changes from upstream
|
file |
diff |
annotate
|
| Fri, 16 May 2014 08:38:23 +0100 |
Christian Urban |
updated changes from upstream (AFP)
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 15:31:17 +0000 |
Christian Urban |
updated to massive changes in Isabelle
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 09:21:31 +0000 |
Christian Urban |
updated to Isabelle changes
|
file |
diff |
annotate
|
| Mon, 13 Jan 2014 15:42:10 +0000 |
Christian Urban |
fixed bug with support and freshness lemmas not being simplified properly
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 23:17:23 +0000 |
Christian Urban |
updated with current AFP version
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 15:14:40 +1100 |
Christian Urban |
updated to 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
|
| Thu, 04 Oct 2012 12:44:43 +0100 |
Christian Urban |
removed "use" - replaced by "ML_file"
|
file |
diff |
annotate
|
| Mon, 18 Jun 2012 14:50:02 +0100 |
Christian Urban |
used ML-antiquotation command_spec for new commands
|
file |
diff |
annotate
|
| Thu, 31 May 2012 12:01:01 +0100 |
Christian Urban |
added to the simplifier nominal_datatype.fresh lemmas
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 18:58:03 +0200 |
Cezary Kaliszyk |
Find remaining rsp theorems and provide them with the quotient definitions
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 15:58:13 +0200 |
Cezary Kaliszyk |
Declare rsp for permute, permute_bn, alpha_bn together with their definitions instead of TrueI
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 15:28:35 +0200 |
Cezary Kaliszyk |
Pass proper rsp theorems for constructors and for size
|
file |
diff |
annotate
|
| Tue, 10 Apr 2012 15:22:16 +0100 |
Christian Urban |
updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 11:26:10 +0000 |
Christian Urban |
updated to new Isabelle (20 March)
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 05:13:59 +0000 |
Christian Urban |
updated to new Isabelle (declared keywords)
|
file |
diff |
annotate
|
| Thu, 22 Dec 2011 13:10:30 +0000 |
Christian Urban |
the default sort for type-variables in nominal specifications is fs; it is automatically addded
|
file |
diff |
annotate
|
| Sun, 18 Dec 2011 00:42:32 +0000 |
Christian Urban |
partially localised the parsing process using functions fron Datatype
|
file |
diff |
annotate
|
| Sat, 17 Dec 2011 16:36:51 +0000 |
Christian Urban |
Started Nominal2-Isabelle2011-1 branch and backported changeset 32abaea424bd
Nominal2-Isabelle2011-1
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 16:20:42 +0000 |
Christian Urban |
updated to lates changes in the datatype package
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 01:32:42 +0000 |
Christian Urban |
generated the correct thm-list for showing that qfv are equal to support
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 09:39:56 +0000 |
Christian Urban |
updated to Isabelle 13 Dec
|
file |
diff |
annotate
|
| Tue, 06 Dec 2011 23:42:19 +0000 |
Christian Urban |
updated to Isabelle 6 Dec (thanks to Odrej Kuncar)
|
file |
diff |
annotate
|