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