Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
Mon, 31 Jan 2022 16:09:23 +0100 blanchet implemented 'max_proofs' mechanism file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet crude implementation of centralized slicing file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet rationalize slicing format file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet thread slices through file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet simplified 'best_slice' data structure and made minor changes to slices file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet changed logic of 'slice' option to 'slices' file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet rationalized output for forthcoming slicing model file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet disable slicing within SMT (in preparation for factoring it out) file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet generalized the 'slice' option towards more flexible slicing file | diff | annotate
Thu, 08 Jul 2021 15:25:30 +0200 desharna promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules" file | diff | annotate
Thu, 08 Oct 2020 17:02:56 +0200 desharna tune filename file | diff | annotate
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches; file | diff | annotate
Sun, 14 Aug 2016 12:26:09 +0200 blanchet killed final stops in Sledgehammer and friends file | diff | annotate
Mon, 28 Mar 2016 12:05:47 +0200 blanchet early warning when Sledgehammer finds a proof file | diff | annotate
Fri, 02 Oct 2015 21:06:32 +0200 blanchet removed legacy asynchronous mode in Sledgehammer file | diff | annotate
Thu, 13 Aug 2015 11:05:19 +0200 wenzelm tuned signature, in accordance to sortBy in Scala; file | diff | annotate
Wed, 14 Jan 2015 01:42:36 +0100 blanchet don't minimize chained facts -- this leads to subtle failures, e.g. if a method succeeds without a chained fact but fails with it file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message; file | diff | annotate
Sun, 12 Oct 2014 21:52:45 +0200 blanchet special treatment of extensionality in minimizer file | diff | annotate
Tue, 30 Sep 2014 14:18:07 +0200 blanchet always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof') file | diff | annotate
Thu, 28 Aug 2014 16:58:27 +0200 blanchet merged minimize and auto_minimize file | diff | annotate
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT' file | diff | annotate
Mon, 04 Aug 2014 13:48:05 +0200 blanchet restored more sorting file | diff | annotate
Mon, 04 Aug 2014 12:28:42 +0200 blanchet rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet restored a bit of laziness file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tuning file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated needlessly complex message tail file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated Sledgehammer's "min" subcommand (and lots of complications in the code) file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet rationalized preplaying by eliminating (now superfluous) laziness file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet simplified minimization logic file | diff | annotate
Wed, 30 Jul 2014 23:52:56 +0200 blanchet use parallel preplay machinery also for one-line proofs file | diff | annotate
Wed, 30 Jul 2014 23:52:56 +0200 blanchet always minimize Sledgehammer results by default file | diff | annotate
Fri, 25 Jul 2014 11:26:23 +0200 blanchet don't lose 'minimize' flag before it reaches Isar proof text generation file | diff | annotate
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options file | diff | annotate
Wed, 11 Jun 2014 11:28:46 +0200 blanchet removed old SMT module from Sledgehammer file | diff | annotate
Thu, 22 May 2014 03:29:36 +0200 blanchet tuning file | diff | annotate
Fri, 16 May 2014 19:14:00 +0200 blanchet correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs file | diff | annotate
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer file | diff | annotate
Thu, 13 Feb 2014 13:16:17 +0100 blanchet avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures file | diff | annotate
Mon, 03 Feb 2014 23:38:33 +0100 blanchet properly overwrite replay data from one compression iteration to another file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover file | diff | annotate
Mon, 03 Feb 2014 17:13:31 +0100 blanchet added 'smt' option to control generation of 'by smt' proofs file | diff | annotate
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file file | diff | annotate
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' file | diff | annotate
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 12:30:54 +0100 blanchet refactor large ML file file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure file | diff | annotate | base
less more (0) tip
isabelle