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 |