| Wed, 11 Dec 2013 20:38:39 +0100 | wenzelm | tuned patterns; | changeset | files |
| Wed, 11 Dec 2013 18:02:22 +0100 | wenzelm | support for polml-5.5.2; | changeset | files |
| Wed, 11 Dec 2013 22:53:32 +0800 | blanchet | reverse order in which lines are selected, to ensure that the number of dependencies is accurate | changeset | files |
| Wed, 11 Dec 2013 22:23:42 +0800 | blanchet | truncate proof once False is hit to avoid confusing the rest of the code (no idea why Z3 goes on) | changeset | files |
| Wed, 11 Dec 2013 22:23:07 +0800 | blanchet | removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas | changeset | files |
| Wed, 11 Dec 2013 00:17:09 +0000 | paulson | Fib: Who needs the int version? | changeset | files |
| Tue, 10 Dec 2013 15:24:17 +0800 | blanchet | more work on Z3 Isar proofs | changeset | files |