| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
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
|
| Wed, 12 Mar 2008 11:57:12 +0100 |
urbanc |
tuned
|
file |
diff |
annotate
|
| Mon, 11 Feb 2008 15:19:17 +0100 |
urbanc |
tuned proofs and comments
|
file |
diff |
annotate
|
| Tue, 01 Jan 2008 07:28:20 +0100 |
urbanc |
tuned proofs and comments
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 01:07:21 +0100 |
urbanc |
polishing of some proofs
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 19:12:05 +0200 |
urbanc |
further comments
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 19:04:53 +0200 |
urbanc |
polished the proofs and added a version of the weakening lemma that does not use the variable convention
|
file |
diff |
annotate
|
| Sun, 12 Aug 2007 18:53:03 +0200 |
wenzelm |
added type constraints to resolve syntax ambiguities;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:36:06 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
file |
diff |
annotate
|
| 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
|