| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | added a new version of 'metis' to the mix | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | implemented new 'try0_isar' semantics | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | tuning | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | better time slack, to account for ultra-quick proof methods | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | crucial fix: use right version of the step | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | more thorough, hybrid compression | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | tuning | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | got rid of 'try0' step that is now redundant | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | centralize more preplaying | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | tuning | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | centralize preplaying | changeset | files |
| Mon, 03 Feb 2014 10:14:18 +0100 | blanchet | tuned | changeset | files |
| Mon, 03 Feb 2014 00:22:48 +0000 | paulson | fixed indentation | changeset | files |
| Sun, 02 Feb 2014 21:48:28 +0000 | paulson | new lemmas involving phi from Lehmer AFP entry | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | more data structure rationalization | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | tuning | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | more data structure rationalization | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | rationalized threading of 'metis' arguments | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | refactored data structure (step 3) | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | refactoring of data structure (step 2) | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | 'primitive' is not an adverb | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | unform treatment of preplay_timeout = 0 and > 0 | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | refactor data structure (step 1) | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | tuned code | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | tuned factor | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | tuning | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | made SML/NJ happier | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | take intersection rather than union of methods when merging steps -- more efficient and natural | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | merge proof methods | changeset | files |
| Sun, 02 Feb 2014 20:53:51 +0100 | blanchet | use Skolem proof methods appropriately | changeset | files |