Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
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
Tue, 03 Mar 2015 16:37:45 +0100 blanchet SPASS-Pirate is now called Pirate file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Sun, 12 Oct 2014 21:52:45 +0200 blanchet improved handling of extensionality in Isar proofs generated from LEO-II and Satallax file | diff | annotate
Sun, 12 Oct 2014 21:52:44 +0200 blanchet made SML/NJ happier file | diff | annotate
Mon, 06 Oct 2014 19:19:16 +0200 blanchet avoid creating needless skolemization steps for SPASS file | diff | annotate
Mon, 06 Oct 2014 19:19:16 +0200 blanchet get rid of 'individual' type in DFG proofs file | diff | annotate
Mon, 06 Oct 2014 19:19:16 +0200 blanchet slightly nicer names file | diff | annotate
Mon, 06 Oct 2014 19:19:16 +0200 blanchet improved unskolemization of SPASS problems file | diff | annotate
Tue, 30 Sep 2014 16:01:46 +0200 blanchet proper types for applied variables, for typed formats (TFF0, DFG) file | diff | annotate
Mon, 29 Sep 2014 20:26:04 +0200 blanchet support hypotheses with schematics in Isar proofs file | diff | annotate
Mon, 29 Sep 2014 10:39:39 +0200 blanchet parse back type of SPASS proof variables file | diff | annotate
Thu, 28 Aug 2014 23:48:46 +0200 blanchet reworked unskolemization for SPASS file | diff | annotate
Sat, 09 Aug 2014 21:03:42 +0200 wenzelm tuned; file | diff | annotate
Tue, 05 Aug 2014 10:59:40 +0200 blanchet rationalize Skolem names file | diff | annotate
Tue, 05 Aug 2014 10:02:35 +0200 blanchet tuned code file | diff | annotate
Tue, 05 Aug 2014 09:58:23 +0200 blanchet don't rename variables which will be renamed later anyway file | diff | annotate
Tue, 05 Aug 2014 09:55:42 +0200 blanchet normalize skolem argument variable names so that they coincide when taking the conjunction file | diff | annotate
Tue, 05 Aug 2014 09:20:00 +0200 blanchet tuning file | diff | annotate
Mon, 04 Aug 2014 16:53:09 +0200 blanchet deal with E definitions file | diff | annotate
Fri, 01 Aug 2014 23:29:50 +0200 blanchet fine-tuned Isar reconstruction, esp. boolean simplifications file | diff | annotate
Fri, 01 Aug 2014 23:29:49 +0200 blanchet centralized boolean simplification so that e.g. LEO-II benefits from it file | diff | annotate
Fri, 01 Aug 2014 20:44:29 +0200 blanchet better handling of variable names file | diff | annotate
Wed, 30 Jul 2014 23:52:56 +0200 blanchet unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings) file | diff | annotate
Wed, 30 Jul 2014 14:03:13 +0200 fleury Whitespace and indentation correction. file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch hilbert_choice_support file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch satallax_proof_support_Sledgehammer file | diff | annotate
Wed, 30 Jul 2014 14:03:11 +0200 fleury removing the '= True' generated by Leo-II. file | diff | annotate
Wed, 30 Jul 2014 00:50:41 +0200 blanchet also try 'metis' with 'full_types' file | diff | annotate
Mon, 28 Jul 2014 10:57:33 +0200 blanchet correctly translate THF functions from terms to types file | diff | annotate
Thu, 24 Jul 2014 00:24:00 +0200 blanchet more robust handling of types for skolems (modeled as Frees) file | diff | annotate
Sat, 12 Jul 2014 11:31:23 +0200 blanchet don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax file | diff | annotate
Mon, 16 Jun 2014 19:42:44 +0200 blanchet integrated new Waldmeister code with 'sledgehammer' command file | diff | annotate
Mon, 16 Jun 2014 19:40:59 +0200 blanchet simplified code file | diff | annotate
Mon, 16 Jun 2014 16:21:52 +0200 fleury Moving the remote prefix deleting on Sledgehammer's side file | diff | annotate
Mon, 16 Jun 2014 16:21:39 +0200 fleury Correcting the type parser file | diff | annotate
Mon, 16 Jun 2014 16:18:34 +0200 fleury imported patch leo2_skolem_simplication file | diff | annotate
Mon, 16 Jun 2014 16:18:15 +0200 fleury add support for Isar reconstruction for thf1 ATP provers like Leo-II. file | diff | annotate
Tue, 10 Jun 2014 11:38:53 +0200 blanchet tuning file | diff | annotate
less more (0) -100 -60 tip
isabelle