Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
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 run all installed provers by default 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 implemented 'max_proofs' mechanism 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 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
Sat, 18 Dec 2021 13:27:42 +0100 desharna proper filtering inf induction rules in Mirabelle file | diff | annotate
Fri, 17 Dec 2021 09:51:37 +0100 desharna added support for initialization messages to Mirabelle file | diff | annotate
Sun, 28 Nov 2021 14:15:01 +0100 desharna reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle file | diff | annotate
Tue, 28 Sep 2021 10:47:18 +0200 desharna prefer veriT over Z3 in sledgehammer 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
Tue, 01 Dec 2020 15:29:54 +0100 desharna tuned proof preplay to explicitly refer to Z3 backend file | diff | annotate
Thu, 29 Oct 2020 16:07:41 +0100 desharna Added smt (verit) to Sledgehammer's proof preplay. file | diff | annotate
Thu, 08 Oct 2020 17:02:56 +0200 desharna tune filename file | diff | annotate
Wed, 10 Jun 2020 15:55:41 +0200 blanchet simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais) 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, 29 Jan 2015 16:35:29 +0100 wenzelm more explicit indication of Async_Manager_Legacy as Proof General legacy; 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:54:14 +0200 blanchet tuned output in case of one-liner failure file | diff | annotate
Thu, 28 Aug 2014 23:57:26 +0200 blanchet renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods 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 15:02:02 +0200 blanchet cleaner 'compress' option 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 honor 'try0' also for one-liners file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence 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 put faster proof methods first 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
Wed, 30 Jul 2014 23:52:56 +0200 blanchet added more proof methods for one-liners 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 Basic support for the SMT prover veriT. 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
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover file | diff | annotate
Thu, 22 May 2014 05:23:50 +0200 blanchet properly reconstruct helpers in Z3 proofs file | diff | annotate
Thu, 22 May 2014 03:29:36 +0200 blanchet tuning file | diff | annotate
Wed, 21 May 2014 14:09:42 +0200 blanchet avoid markup-generating @{make_string} 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
Fri, 16 May 2014 19:13:50 +0200 blanchet use 'simp add:' syntax in Sledgehammer rather than 'using' file | diff | annotate
Fri, 14 Mar 2014 12:09:51 +0100 blanchet delayed construction of command (and of noncommercial check) + tuning file | diff | annotate
Thu, 13 Mar 2014 13:18:14 +0100 blanchet simplified preplaying information file | diff | annotate
Thu, 13 Mar 2014 13:18:13 +0100 blanchet honor the fact that the new Z3 can generate Isar proofs file | diff | annotate
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer file | diff | annotate
Fri, 14 Feb 2014 10:33:57 +0100 blanchet restored old 'remotify' logic -- too many bugs were introduced when refactoring the code file | diff | annotate
Thu, 13 Feb 2014 16:21:43 +0100 blanchet do the right thing with provers that exist only remotely (e.g. e_sine) file | diff | annotate
Thu, 13 Feb 2014 13:16:17 +0100 blanchet repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial file | diff | annotate
less more (0) -60 tip
isabelle