| Wed, 04 Apr 2007 19:56:25 +0200 |
narboux |
add a few details in the Fst and Snd cases of unicity proof
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 19:16:11 +0200 |
berghofe |
- Renamed <predicate>_eqvt to <predicate>.eqvt
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 01:55:18 +0200 |
urbanc |
tuned proofs (taking full advantage of nominal_inductive)
|
file |
diff |
annotate
|
| Tue, 27 Mar 2007 17:57:05 +0200 |
berghofe |
Adapted to changes in nominal_inductive.
|
file |
diff |
annotate
|
| Thu, 22 Mar 2007 16:34:03 +0100 |
krauss |
fixed function syntax
|
file |
diff |
annotate
|
| Thu, 22 Mar 2007 10:35:12 +0100 |
urbanc |
tuned some proofs
|
file |
diff |
annotate
|
| Wed, 21 Mar 2007 16:06:15 +0100 |
krauss |
Unified function syntax
|
file |
diff |
annotate
|
| Tue, 06 Mar 2007 16:40:32 +0100 |
narboux |
correct typo in latex output
|
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
|
| Wed, 17 Jan 2007 19:29:55 +0100 |
urbanc |
tuned a bit the proofs
|
file |
diff |
annotate
|
| Tue, 16 Jan 2007 13:59:08 +0100 |
urbanc |
formalisation of Crary's chapter on logical relations
|
file |
diff |
annotate
|