| Fri, 30 Mar 2007 16:19:00 +0200 |
haftmann |
paraphrasing equality
|
changeset |
files
|
| Fri, 30 Mar 2007 16:18:59 +0200 |
haftmann |
updated
|
changeset |
files
|
| Thu, 29 Mar 2007 14:21:47 +0200 |
haftmann |
improved character output for SML
|
changeset |
files
|
| Thu, 29 Mar 2007 14:21:45 +0200 |
haftmann |
dropped legacy ML bindings
|
changeset |
files
|
| Thu, 29 Mar 2007 11:59:54 +0200 |
paulson |
simplified some steps
|
changeset |
files
|
| 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
|
| Wed, 28 Mar 2007 17:27:44 +0200 |
urbanc |
adapted to new nominal_inductive
|
changeset |
files
|