| Wed, 28 Mar 2007 19:17:40 +0200 |
berghofe |
Renamed induct(s)_weak to weak_induct(s) in order to unify
|
changeset |
files
|
| Wed, 28 Mar 2007 19:16:11 +0200 |
berghofe |
- Renamed <predicate>_eqvt to <predicate>.eqvt
|
changeset |
files
|
| Wed, 28 Mar 2007 18:25:23 +0200 |
urbanc |
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
|
changeset |
files
|
| Wed, 28 Mar 2007 17:27:44 +0200 |
urbanc |
adapted to new nominal_inductive
|
changeset |
files
|
| Wed, 28 Mar 2007 10:47:19 +0200 |
berghofe |
Improved code generator for characters: now handles
|
changeset |
files
|
| Wed, 28 Mar 2007 01:55:18 +0200 |
urbanc |
tuned proofs (taking full advantage of nominal_inductive)
|
changeset |
files
|
| Wed, 28 Mar 2007 01:29:43 +0200 |
urbanc |
adapted to nominal_inductive infrastructure
|
changeset |
files
|
| Wed, 28 Mar 2007 01:09:23 +0200 |
urbanc |
made the type sets instance of the "cp" type-class
|
changeset |
files
|
| Tue, 27 Mar 2007 19:39:40 +0200 |
urbanc |
added extended the lemma for equivariance of freshness
|
changeset |
files
|
| Tue, 27 Mar 2007 19:13:28 +0200 |
urbanc |
adapted to nominal_inductive
|
changeset |
files
|
| Tue, 27 Mar 2007 18:28:22 +0200 |
urbanc |
adapted to new nominal_inductive infrastructure
|
changeset |
files
|
| Tue, 27 Mar 2007 17:57:42 +0200 |
berghofe |
Adapted to new syntax of nominal_inductive.
|
changeset |
files
|