| Sun, 01 Dec 2024 14:24:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 22:33:21 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 25 Oct 2024 15:31:58 +0200 |
blanchet |
variable instantiation in Sledgehammer and Metis
|
file |
diff |
annotate
|
| Tue, 27 Feb 2024 14:08:28 +0100 |
blanchet |
support Zipperposition's skolemization in generated Isar proofs
|
file |
diff |
annotate
|
| Mon, 26 Feb 2024 13:10:37 +0100 |
blanchet |
deal with new-style Vampire skolemization in reconstructed Isar proofs
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 17:16:32 +0200 |
blanchet |
avoid legacy binding errors in Sledgehammer Isar proofs
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 17:16:32 +0200 |
blanchet |
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 17:16:32 +0200 |
blanchet |
reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
|
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
|
| Wed, 08 Mar 2023 17:51:56 +0100 |
blanchet |
require the presence of free variables to do abduction in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
tweaked Sledgehammer interaction
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
reverted 0506c3273814 -- the message is still useful
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
tweaked abduction in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
improve ad hoc abduction in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
implemented ad hoc abduction in Sledgehammer with E
|
file |
diff |
annotate
|
| Wed, 15 Feb 2023 17:01:42 +0100 |
blanchet |
removed rarely used error in Sledgehammer
|
file |
diff |
annotate
|
| Tue, 22 Feb 2022 12:36:01 +0100 |
blanchet |
handle Zipperposition definitions in Isar proof construction
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 12:48:33 +0100 |
blanchet |
careful with partial applications
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 11:51:41 +0100 |
blanchet |
handle TPTP '!=' more gracefully in Isar proof reconstruction
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 22:08:51 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Mon, 19 Jul 2021 14:47:53 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 17 Dec 2020 15:31:31 +0100 |
desharna |
tweaked tptp parsing when source info is missing
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:46:03 +0200 |
blanchet |
removed obsolete unmaintained experimental prover Pirate
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 15:59:25 +0200 |
blanchet |
added support for Zipperposition on SystemOnTPTP
|
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, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|