| Tue, 04 Feb 2014 23:11:18 +0100 | blanchet | tweaked handling of 'hopeless' methods | changeset | files |
| Tue, 04 Feb 2014 23:11:18 +0100 | blanchet | do a second phase of proof compression after minimization | changeset | files |
| Tue, 04 Feb 2014 23:11:18 +0100 | blanchet | don't give up on hopeless proof methods -- they can become hopeful again | changeset | files |
| Tue, 04 Feb 2014 23:11:18 +0100 | blanchet | tuned code | changeset | files |
| Tue, 04 Feb 2014 23:11:18 +0100 | blanchet | tuned slack | changeset | files |
| Tue, 04 Feb 2014 23:11:18 +0100 | blanchet | split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed) | changeset | files |
| Tue, 04 Feb 2014 21:29:46 +0000 | paulson | removal of "back", etc. | changeset | files |