| Sat, 07 Aug 2021 22:23:37 +0200 |
wenzelm |
clarified signature: more options for bash_process;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Sun, 25 Apr 2021 22:33:15 +0200 |
wenzelm |
avoid "exec" to change the winpid;
|
file |
diff |
annotate
|
| Mon, 12 Apr 2021 22:16:31 +0200 |
wenzelm |
clarified signature: more structured arguments, notably for remote provers;
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 20:29:26 +0100 |
wenzelm |
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 16:50:11 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2021 19:29:45 +0100 |
wenzelm |
more direct elapsed run_time via bash_process wrapper (via Scala and C);
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 10:10:44 +0100 |
desharna |
tuned exec field in atp_config
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 16:07:41 +0100 |
desharna |
Added smt (verit) to Sledgehammer's proof preplay.
|
file |
diff |
annotate
|
| Tue, 27 Oct 2020 22:34:37 +0100 |
wenzelm |
clarified signature: overloaded "+" for Path.append;
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:46:03 +0200 |
blanchet |
removed obsolete unmaintained experimental prover Pirate
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:02:56 +0200 |
desharna |
tune filename
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 16:36:00 +0200 |
desharna |
drop obsolete ad hoc support for Satallax isar proof reconstruction
|
file |
diff |
annotate
|
| Wed, 10 Jun 2020 15:55:41 +0200 |
blanchet |
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 14:14:56 +0200 |
blanchet |
removed experimental encoding for Waldmeister
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 23:29:05 +0200 |
wenzelm |
prefer infix operations;
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
early warning when Sledgehammer finds a proof
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
refined experimental option of Sledgehammer
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 21:09:28 +0100 |
wenzelm |
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:41:14 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 20:02:51 +0100 |
blanchet |
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 21:46:48 +0200 |
blanchet |
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
|
file |
diff |
annotate
|
| Wed, 19 Aug 2015 20:41:23 +0200 |
wenzelm |
proper check for Windows executables;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 16:37:45 +0100 |
blanchet |
SPASS-Pirate is now called Pirate
|
file |
diff |
annotate
|