| 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
|
| 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
|
| 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
|
| Mon, 28 May 2012 18:03:06 +0100 |
Christian Urban |
added library routines for the constant fresh
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 09:39:56 +0000 |
Christian Urban |
updated to Isabelle 13 Dec
|
file |
diff |
annotate
|
| Sat, 26 Nov 2011 09:48:14 +0000 |
Christian Urban |
used simproc-antiquotation
|
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, 22 Jul 2011 11:37:16 +0100 |
Christian Urban |
completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list
|
file |
diff |
annotate
|
| Wed, 22 Jun 2011 14:14:54 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Wed, 22 Jun 2011 13:40:25 +0100 |
Christian Urban |
deleted some dead code
|
file |
diff |
annotate
|
| Thu, 16 Jun 2011 20:07:03 +0100 |
Christian Urban |
got rid of the boolean flag in the raw_equivariance function
|
file |
diff |
annotate
|
| Mon, 28 Feb 2011 15:21:10 +0000 |
Christian Urban |
split the library into a basics file; merged Nominal_Eqvt into Nominal_Base
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 19:57:57 +0000 |
Christian Urban |
removed debugging code abd introduced a guarded tracing function
|
file |
diff |
annotate
|
| Tue, 04 Jan 2011 13:47:38 +0000 |
Christian Urban |
final version of the ESOP paper; used set+ instead of res as requested by one reviewer
|
file |
diff |
annotate
|
| Mon, 03 Jan 2011 16:19:27 +0000 |
Christian Urban |
simple cases for string rule inductions
|
file |
diff |
annotate
|
| Tue, 28 Dec 2010 19:51:25 +0000 |
Christian Urban |
automated all strong induction lemmas
|
file |
diff |
annotate
|
| Thu, 23 Dec 2010 00:22:41 +0000 |
Christian Urban |
moved generic functions into nominal_library
|
file |
diff |
annotate
|
| Wed, 22 Dec 2010 12:47:09 +0000 |
Christian Urban |
updated to Isabelle 22 December
|
file |
diff |
annotate
|
| Wed, 22 Dec 2010 12:17:49 +0000 |
Christian Urban |
a bit tuning
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 10:28:08 +0000 |
Christian Urban |
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 01:01:44 +0000 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 08:42:48 +0000 |
Christian Urban |
simple cases for strong inducts done; infrastructure for the difficult ones is there
|
file |
diff |
annotate
|
| Tue, 14 Dec 2010 14:23:40 +0000 |
Christian Urban |
freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 22:09:11 +0000 |
Christian Urban |
created strong_exhausts terms
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 00:10:40 +0000 |
Christian Urban |
moved setify and listify functions into the library; introduced versions that have a type argument
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 17:07:08 +0000 |
Christian Urban |
first tests about exhaust
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:16:25 +0000 |
Christian Urban |
moved some code into the nominal_library
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 14:24:17 +0000 |
Christian Urban |
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 09:52:29 +0000 |
Christian Urban |
proved that bn functions return a finite set
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 01:10:02 +0000 |
Christian Urban |
fixed bug in fv function where a shallow binder binds lists of names
|
file |
diff |
annotate
|
| Sun, 14 Nov 2010 16:34:47 +0000 |
Christian Urban |
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
|
file |
diff |
annotate
| base
|