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/Sledgehammer/sledgehammer.ML
Tue, 01 Feb 2022 17:11:26 +0100 blanchet propagate right result when enough proofs have been found file | diff | annotate
Tue, 01 Feb 2022 14:54:31 +0100 blanchet don't lose error messages file | diff | annotate
Tue, 01 Feb 2022 09:21:50 +0100 blanchet tuning file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet tweaked Auto Sledgehammer's behavior and output file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet print more verbose information file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet run all installed provers by default file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet update slice options centrally file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet further work on new Sledgehammer slicing file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet tweaked verbose output file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet tweak padding of prover slice schedule to include all provers file | diff | annotate
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 document new option 'max_proofs' 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 take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set 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 rationalized output for forthcoming slicing model file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code 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
Sat, 22 Jan 2022 11:33:31 +0100 desharna added spying of fact filtering timing file | diff | annotate
Fri, 21 Jan 2022 16:17:42 +0100 desharna added syping of fact filtering time to sledgehammer file | diff | annotate
Sat, 18 Dec 2021 23:11:49 +0100 desharna tuned run_sledgehammer and called it directly from Mirabelle file | diff | annotate
Sat, 18 Dec 2021 14:30:13 +0100 desharna exported Sledgehammer.launch_prover and use it in Mirabelle file | diff | annotate
Sat, 18 Dec 2021 13:27:42 +0100 desharna proper filtering inf induction rules in Mirabelle file | diff | annotate
Fri, 17 Dec 2021 09:57:22 +0100 desharna added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle file | diff | annotate
Tue, 13 Jul 2021 10:57:15 +0200 blanchet revisited ac28714b7478: more faithful preplaying with chained facts file | diff | annotate
Thu, 08 Jul 2021 17:23:01 +0200 desharna refactored Sledgehammer option "induction_rules" file | diff | annotate
Thu, 08 Jul 2021 15:25:30 +0200 desharna promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules" file | diff | annotate
Fri, 05 Mar 2021 16:09:42 +0100 wenzelm clarified signature --- augment existing structure Time; file | diff | annotate
Thu, 22 Oct 2020 15:18:08 +0200 desharna Tuned isar_step datatype file | diff | annotate
Thu, 23 Apr 2020 16:52:14 +0200 blanchet avoid passing chained facts twice to preplay in Sledgehammer file | diff | annotate
Mon, 21 Jan 2019 22:29:41 +0100 blanchet get rid of visibility in MaSh -- it slows it down more than it helps file | diff | annotate
Sun, 14 Aug 2016 12:26:09 +0200 blanchet avoid loading MaSh file first time around for higher responsiveness of Sledgehammer file | diff | annotate
Sun, 14 Aug 2016 12:26:09 +0200 blanchet optimization in MaSh parsing file | diff | annotate
Sun, 14 Aug 2016 12:26:09 +0200 blanchet tuned ML file | diff | annotate
Sun, 14 Aug 2016 12:26:09 +0200 blanchet killed final stops in Sledgehammer and friends file | diff | annotate
Fri, 17 Jun 2016 12:40:18 +0200 blanchet be more careful before filtering out chained facts in Sledgehammer file | diff | annotate
Tue, 17 May 2016 08:40:24 +0200 blanchet proper consideration of chained facts in 'try0' minimization file | diff | annotate
Mon, 28 Mar 2016 12:05:47 +0200 blanchet a more generous hard timeout file | diff | annotate
Mon, 28 Mar 2016 12:05:47 +0200 blanchet early warning when Sledgehammer finds a proof file | diff | annotate
Sat, 05 Mar 2016 17:01:45 +0100 wenzelm tuned signature -- clarified modules; file | diff | annotate
Thu, 03 Mar 2016 15:23:02 +0100 wenzelm clarified modules; file | diff | annotate
Mon, 01 Feb 2016 19:57:58 +0100 blanchet preplaying of 'smt' and 'metis' more in sync with actual method file | diff | annotate
Mon, 05 Oct 2015 23:03:50 +0200 blanchet further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes file | diff | annotate
Fri, 02 Oct 2015 21:15:25 +0200 blanchet further reduced dependency on legacy async thread manager file | diff | annotate
Fri, 02 Oct 2015 21:06:32 +0200 blanchet removed legacy asynchronous mode in Sledgehammer file | diff | annotate
Mon, 21 Sep 2015 23:22:11 +0200 wenzelm clarified markup; file | diff | annotate
Mon, 29 Jun 2015 23:44:53 +0200 blanchet removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs file | diff | annotate
Mon, 22 Jun 2015 16:56:03 +0200 blanchet keep 'Pure.all' in goals when preplaying file | diff | annotate
Mon, 22 Jun 2015 16:56:03 +0200 blanchet use right context for preplay, to avoid errors in fact lookup file | diff | annotate
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names; file | diff | annotate
Thu, 29 Jan 2015 16:35:29 +0100 wenzelm more explicit indication of Async_Manager_Legacy as Proof General legacy; file | diff | annotate
Tue, 23 Dec 2014 20:46:42 +0100 wenzelm explicit message channels for "state", "information"; 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, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; file | diff | annotate
Thu, 06 Nov 2014 13:36:19 +0100 wenzelm prefer explicit Keyword.keywords; file | diff | annotate
Mon, 03 Nov 2014 14:31:15 +0100 wenzelm eliminated obsolete Proof.goal_message -- print outcome more directly; file | diff | annotate
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message; file | diff | annotate
Tue, 30 Sep 2014 16:40:03 +0200 blanchet don't call 'hd' on a possibly empty list file | diff | annotate
Mon, 04 Aug 2014 13:06:24 +0200 blanchet default on 'metis' for ATPs if preplaying is disabled file | diff | annotate
less more (0) -100 -60 tip
isabelle