| Thu, 02 Oct 2014 18:10:09 +0200 | blanchet | more precise lemma insertion | changeset | files |
| Thu, 02 Oct 2014 17:40:46 +0200 | blanchet | insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem | changeset | files |
| Thu, 02 Oct 2014 17:39:38 +0200 | blanchet | avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition | changeset | files |
| Thu, 02 Oct 2014 15:24:51 +0200 | blanchet | eliminate duplicate hypotheses (which can arise due to (un)clausification) | changeset | files |