| Tue, 24 Jun 2014 08:19:22 +0200 | blanchet | supports gradual skolemization (cf. Z3) by threading context through correctly | changeset | files |
| 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 |
| Sun, 22 Jun 2014 12:37:55 +0200 | nipkow | r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs | changeset | files |
| Sat, 21 Jun 2014 15:46:52 +0200 | nipkow | added [simp] | changeset | files |
| Sat, 21 Jun 2014 10:41:02 +0200 | ballarin | Two basic lemmas on bij_betw. | changeset | files |