| Wed, 06 Jun 2012 21:36:21 +0200 | krauss | fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users | changeset | files |
| Wed, 06 Jun 2012 10:35:05 +0200 | blanchet | tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings | changeset | files |
| Wed, 06 Jun 2012 10:35:05 +0200 | blanchet | pass more facts to LEO-II, in the light of latest evaluation | changeset | files |