| 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
|