| 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
|
| Thu, 08 Oct 2020 17:55:17 +0200 |
blanchet |
removed support for obsolete prover SNARK and underperforming prover E-Par
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:02:56 +0200 |
desharna |
tune filename
|
file |
diff |
annotate
|
| Tue, 08 Sep 2020 11:32:57 +0200 |
desharna |
[mirabelle] add initial documentation in Sledgehammer's doc
|
file |
diff |
annotate
|
| Thu, 23 Apr 2020 15:45:42 +0200 |
blanchet |
tweaked Vampire's options + tuning
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 16:28:04 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 14:55:14 +0200 |
blanchet |
removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 09:57:20 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Thu, 29 Jan 2015 16:35:29 +0100 |
wenzelm |
more explicit indication of Async_Manager_Legacy as Proof General legacy;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 14:32:30 +0200 |
blanchet |
made 'moura' tactic more powerful
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
moved skolem method
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:41:42 +0200 |
blanchet |
fixed parsing of one-argument 'file()' in TSTP files
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:41:01 +0200 |
blanchet |
use right delimiters for Waldmeister proofs
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:40:59 +0200 |
blanchet |
simplified code
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:40:04 +0200 |
blanchet |
moved code around
|
file |
diff |
annotate
|