| 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
|
| Sun, 02 Jul 2006 17:27:10 +0200 |
urbanc |
added more infrastructure for the recursion combinator
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 15:58:30 +0200 |
berghofe |
Capitalized theory names.
|
file |
diff |
annotate
|
| Wed, 11 Jan 2006 17:07:57 +0100 |
urbanc |
tuned proofs
|
file |
diff |
annotate
|
| Wed, 11 Jan 2006 14:00:11 +0100 |
urbanc |
tuned the eqvt-proof
|
file |
diff |
annotate
|
| Mon, 05 Dec 2005 17:02:20 +0100 |
urbanc |
tuned
|
file |
diff |
annotate
|
| Mon, 05 Dec 2005 10:33:30 +0100 |
urbanc |
tuned
|
file |
diff |
annotate
|
| Sun, 04 Dec 2005 12:14:40 +0100 |
urbanc |
tuned
|
file |
diff |
annotate
|
| Thu, 01 Dec 2005 04:46:17 +0100 |
urbanc |
changed "fresh:" to "avoiding:" and cleaned up the weakening example
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 14:27:09 +0100 |
urbanc |
adapted to the new nominal_induction
|
file |
diff |
annotate
|
| Mon, 28 Nov 2005 05:03:00 +0100 |
urbanc |
some small tuning
|
file |
diff |
annotate
|
| Mon, 07 Nov 2005 15:12:13 +0100 |
urbanc |
Initial commit of the theory "Weakening".
|
file |
diff |
annotate
|