| Fri, 20 Dec 2013 11:34:07 +0100 | blanchet | note manually proved exclusiveness property | changeset | files |
| Fri, 20 Dec 2013 11:12:51 +0100 | blanchet | note exhaust proof obligation | changeset | files |
| Fri, 20 Dec 2013 09:48:04 +0100 | blanchet | compile | changeset | files |
| Thu, 19 Dec 2013 21:49:30 +0100 | blanchet | implemented 'exhaustive' option in tactic | changeset | files |
| Thu, 19 Dec 2013 20:07:06 +0100 | blanchet | tuning | changeset | files |
| Thu, 19 Dec 2013 19:37:43 +0100 | blanchet | tuning | changeset | files |
| Thu, 19 Dec 2013 19:35:50 +0100 | blanchet | tuning 'case' expressions | changeset | files |
| Thu, 19 Dec 2013 19:16:44 +0100 | blanchet | don't do 'isar_try0' if preplaying is off | changeset | files |
| Thu, 19 Dec 2013 18:39:54 +0100 | blanchet | more data structure refactoring | changeset | files |
| Thu, 19 Dec 2013 18:22:31 +0100 | blanchet | data structure rationalization | changeset | files |
| Thu, 19 Dec 2013 18:07:21 +0100 | blanchet | tuning | changeset | files |
| Thu, 19 Dec 2013 17:52:58 +0100 | blanchet | refactored preplaying outcome data structure | changeset | files |
| Thu, 19 Dec 2013 17:24:17 +0100 | blanchet | distinguish not preplayed & timed out | changeset | files |
| Thu, 19 Dec 2013 17:11:54 +0100 | blanchet | pick up tfree/tvar type from SPASS-Pirate proof | changeset | files |
| Thu, 19 Dec 2013 16:11:20 +0100 | blanchet | tuning | changeset | files |
| Thu, 19 Dec 2013 15:47:17 +0100 | blanchet | extended ATP types with sorts | changeset | files |
| Thu, 19 Dec 2013 15:04:21 +0100 | blanchet | removed debugging output | changeset | files |
| Thu, 19 Dec 2013 14:57:21 +0100 | blanchet | honor SPASS-Pirate type arguments | changeset | files |
| Thu, 19 Dec 2013 13:46:42 +0100 | blanchet | made SML/NJ-friendlier (hopefully) | changeset | files |
| Thu, 19 Dec 2013 13:43:21 +0100 | blanchet | made timeouts in Sledgehammer not be 'option's -- simplified lots of code | changeset | files |
| Thu, 19 Dec 2013 10:15:12 +0100 | blanchet | simplified data structure | changeset | files |
| Thu, 19 Dec 2013 10:12:28 +0100 | blanchet | prevent curl's output to interfere with the prover's output | changeset | files |
| Thu, 19 Dec 2013 09:28:20 +0100 | blanchet | tuning | changeset | files |
| Wed, 18 Dec 2013 22:55:43 +0100 | blanchet | merge | changeset | files |
| Wed, 18 Dec 2013 22:55:20 +0100 | blanchet | parse SPASS-Pirate types | changeset | files |
| Wed, 18 Dec 2013 17:52:52 +0100 | nipkow | merged | changeset | files |
| Wed, 18 Dec 2013 17:52:44 +0100 | nipkow | added lemma | changeset | files |
| Wed, 18 Dec 2013 17:48:48 +0100 | panny | merge | changeset | files |
| Wed, 18 Dec 2013 14:50:25 +0100 | panny | pass down user input in more cases in order to preserve "let"s etc. | changeset | files |
| Wed, 18 Dec 2013 14:06:34 +0100 | panny | pass auto-proved exhaustiveness properties to tactic; | changeset | files |
| Wed, 18 Dec 2013 17:27:17 +0100 | blanchet | merge | changeset | files |
| Wed, 18 Dec 2013 17:26:31 +0100 | blanchet | changed pirate port | changeset | files |