| 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
|