| Thu, 19 Dec 2013 19:16:44 +0100 |
blanchet |
don't do 'isar_try0' if preplaying is off
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 18:39:54 +0100 |
blanchet |
more data structure refactoring
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 18:22:31 +0100 |
blanchet |
data structure rationalization
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 09:28:20 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
robustness in degenerate case + tuning
|
file |
diff |
annotate
|
| Tue, 10 Dec 2013 15:24:17 +0800 |
blanchet |
more work on Z3 Isar proofs
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 06:33:46 +0100 |
blanchet |
adapted code for Z3 proof reconstruction
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 18:38:25 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
merged "isar_try0" and "isar_minimize" options
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 10:26:56 +0200 |
blanchet |
Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 22:41:25 +0200 |
smolkas |
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 19:03:08 +0200 |
smolkas |
cleaner preplay interface
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 14:18:06 +0200 |
smolkas |
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
|
file |
diff |
annotate
|