| Sat, 13 Dec 2008 13:24:45 +0100 |
berghofe |
Modified nominal_primrec to make it work with local theories, unified syntax
|
file |
diff |
annotate
|
| Thu, 22 May 2008 16:34:41 +0200 |
urbanc |
made the naming of the induction principles consistent: weak_induct is
|
file |
diff |
annotate
|
| Mon, 14 Apr 2008 21:44:53 +0200 |
wenzelm |
removed duplicate lemmas;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2008 11:57:12 +0100 |
urbanc |
tuned
|
file |
diff |
annotate
|
| Tue, 01 Jan 2008 07:28:20 +0100 |
urbanc |
tuned proofs and comments
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 23:04:36 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 11:06:04 +0200 |
chaieb |
tuned Proof
|
file |
diff |
annotate
|
| Wed, 02 May 2007 01:42:23 +0200 |
urbanc |
tuned some proofs and changed variable names in some definitions of Nominal.thy
|
file |
diff |
annotate
|
| Tue, 06 Mar 2007 15:28:22 +0100 |
urbanc |
major update of the nominal package; there is now an infrastructure
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 14:05:43 +0100 |
urbanc |
adapted function definitions to new syntax
|
file |
diff |
annotate
|
| Mon, 23 Oct 2006 00:51:16 +0200 |
berghofe |
Adapted to changes in FCBs.
|
file |
diff |
annotate
|
| Wed, 18 Oct 2006 23:15:16 +0200 |
urbanc |
cleaning up
|
file |
diff |
annotate
|
| Fri, 18 Aug 2006 18:46:02 +0200 |
urbanc |
modified to use the characteristic equations
|
file |
diff |
annotate
|
| Thu, 17 Aug 2006 20:31:36 +0200 |
urbanc |
used the recursion combinator for the height and substitution function
|
file |
diff |
annotate
|
| Thu, 01 Jun 2006 14:40:22 +0200 |
urbanc |
added an example suggested by D. Wang on the PoplMark-mailing list;
|
file |
diff |
annotate
|