Sun, 15 Dec 2013 20:31:25 +0100 | blanchet | tuning | changeset | files |
Sun, 15 Dec 2013 20:09:13 +0100 | blanchet | simplify generated propositions | changeset | files |
Sun, 15 Dec 2013 19:01:06 +0100 | blanchet | use 'prop' rather than 'bool' systematically in Isar reconstruction code | changeset | files |
Sun, 15 Dec 2013 18:54:26 +0100 | blanchet | tuning | changeset | files |
Sun, 15 Dec 2013 18:01:38 +0100 | blanchet | use 'arith' when appropriate in Z3 proofs | changeset | files |
Sun, 15 Dec 2013 18:01:38 +0100 | blanchet | robustness in degenerate case + tuning | changeset | files |