| Wed, 15 Mar 2023 15:28:44 +0100 |
blanchet |
removed accidental junk
|
file |
diff |
annotate
|
| Fri, 10 Mar 2023 15:27:18 +0100 |
blanchet |
use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
cleaned up obsolete E setup and a bit of SPASS
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
update slice options centrally
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
further work on new Sledgehammer slicing
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
tweaked verbose output
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
tweak padding of prover slice schedule to include all provers
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
implemented 'max_proofs' mechanism
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
document new option 'max_proofs'
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
crude implementation of centralized slicing
|
file |
diff |
annotate
|
| Wed, 12 May 2021 12:22:44 +0200 |
wenzelm |
avoid duplicate loading of ML file;
|
file |
diff |
annotate
|
| Fri, 12 Mar 2021 23:30:35 +0100 |
wenzelm |
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
|
file |
diff |
annotate
|
| Thu, 12 Nov 2020 17:42:15 +0100 |
desharna |
Removed development code wrongfully committed
|
file |
diff |
annotate
|
| Thu, 05 Nov 2020 18:14:02 +0100 |
desharna |
Added support for TFX to Sledgehammer
|
file |
diff |
annotate
|