| Thu, 19 Apr 2007 16:38:59 +0200 |
berghofe |
nominal_inductive no longer proves equivariance.
|
file |
diff |
annotate
|
| Thu, 12 Apr 2007 15:46:12 +0200 |
urbanc |
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
|
file |
diff |
annotate
|
| Tue, 27 Mar 2007 18:28:22 +0200 |
urbanc |
adapted to new nominal_inductive infrastructure
|
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
|
| Fri, 02 Feb 2007 17:16:16 +0100 |
urbanc |
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 17:52:48 +0100 |
urbanc |
fixed some typos
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 14:11:49 +0100 |
urbanc |
tuned the proof of the strong induction principle
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 17:32:30 +0100 |
urbanc |
added an intro lemma for freshness of products; set up
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 15 Nov 2006 16:23:55 +0100 |
urbanc |
replaced exists_fresh lemma with a version formulated with obtains;
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 22:16:54 +0100 |
wenzelm |
inductive2: canonical specification syntax;
|
file |
diff |
annotate
|
| Mon, 30 Oct 2006 13:07:51 +0100 |
urbanc |
new file for defining functions in the lambda-calculus
|
file |
diff |
annotate
|
| Wed, 18 Oct 2006 23:06:51 +0200 |
urbanc |
adapted to Stefan's new inductive package and cleaning up
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 16:26:59 +0200 |
urbanc |
made some proof look more like the ones in Barendregt
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|