| Thu, 29 Mar 2007 11:12:39 +0200 | paulson | MESON tactical takes an additional argument: the clausification function. | changeset | files |
| Thu, 29 Mar 2007 11:12:03 +0200 | paulson | Now checks for types-only clause before outputting. | changeset | files |
| Wed, 28 Mar 2007 19:18:39 +0200 | berghofe | - Improved error messages in equivariance proof | changeset | files |
| 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 |