| Tue, 24 Jun 2014 08:19:22 +0200 | blanchet | given two one-liners, only show the best of the two | changeset | files |
| Tue, 24 Jun 2014 08:19:22 +0200 | blanchet | don't generate Isar proof skeleton for what amounts to a one-line proof | changeset | files |
| Tue, 24 Jun 2014 08:19:22 +0200 | blanchet | don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof) | changeset | files |