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_proof_methods.ML
Mon, 31 Mar 2025 19:17:51 +0200 desharna tuned file | diff | annotate
Tue, 25 Feb 2025 17:37:41 +0100 desharna initial work on Magnushammer-inspured tactic hammer (from Jasmin) file | diff | annotate
Fri, 25 Oct 2024 15:31:58 +0200 blanchet variable instantiation in Sledgehammer and Metis file | diff | annotate
Fri, 20 Sep 2024 14:28:13 +0200 wenzelm clarified signature: more explicit operations; file | diff | annotate
Wed, 10 Jul 2024 08:37:54 +0200 nipkow take care of facts in cartouches file | diff | annotate
Wed, 29 May 2024 10:43:22 +0200 nipkow pretty-printing sledgehammer command: merge indexed theorems file | diff | annotate
Wed, 20 Mar 2024 12:26:52 +0100 desharna try proof method "order" in Sledgehammer's proof reconstruction file | diff | annotate
Mon, 02 Oct 2023 11:22:53 +0200 desharna used standard Time.compare in Sledgehammer's preplay file | diff | annotate
Mon, 25 Sep 2023 17:16:32 +0200 blanchet added argo file | diff | annotate
Mon, 22 Aug 2022 06:27:28 +0200 Mathias Fleury remove duplicate parsing for alethe; fix skolemization; 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 further work on new Sledgehammer slicing file | diff | annotate
Tue, 13 Jul 2021 10:57:15 +0200 blanchet revisited ac28714b7478: more faithful preplaying with chained facts 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:46:03 +0200 blanchet removed obsolete unmaintained experimental prover Pirate file | diff | annotate
Tue, 20 Aug 2019 11:01:05 +0200 wenzelm clarified signature; file | diff | annotate
Sun, 14 Aug 2016 12:26:09 +0200 blanchet killed final stops in Sledgehammer and friends file | diff | annotate
Sat, 16 Jul 2016 19:35:27 +0200 wenzelm tuned signature; 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
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic; 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
Mon, 01 Jun 2015 18:59:21 +0200 haftmann dropped dead config option file | diff | annotate
Thu, 28 May 2015 09:50:17 +0200 blanchet took out Sledgehammer minimizer optimization that breaks things file | diff | annotate
Sun, 03 May 2015 22:15:29 +0200 blanchet improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this') file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Tue, 30 Sep 2014 15:18:01 +0200 blanchet don't affect other subgoals with 'auto' in one-liner proofs 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 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc. file | diff | annotate
Thu, 28 Aug 2014 16:58:27 +0200 blanchet moved skolem method file | diff | annotate
Thu, 28 Aug 2014 16:58:27 +0200 blanchet added 'skolem' method, esp. for 'obtain's generated from Z3 proofs file | diff | annotate
Thu, 28 Aug 2014 16:58:26 +0200 blanchet tuned method description file | diff | annotate
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT' file | diff | annotate
Sat, 16 Aug 2014 13:23:50 +0200 wenzelm modernized module name and setup; file | diff | annotate
Mon, 04 Aug 2014 12:52:48 +0200 blanchet more informative preplay failures 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 added appropriate method for skolemization of Z3 steps to the mix 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 Sledgehammer's "min" subcommand (and lots of complications in the code) file | diff | annotate
Wed, 30 Jul 2014 23:52:56 +0200 blanchet tuned ML function name file | diff | annotate
Fri, 25 Jul 2014 12:20:48 +0200 blanchet faster minimization by not adding facts that are already in the simpset file | diff | annotate
Fri, 25 Jul 2014 11:31:20 +0200 blanchet added missing facts to proof method file | diff | annotate
Tue, 01 Jul 2014 16:47:10 +0200 blanchet fine-tuned methods file | diff | annotate
Tue, 24 Jun 2014 08:19:55 +0200 blanchet move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects file | diff | annotate
Tue, 24 Jun 2014 08:19:22 +0200 blanchet given two one-liners, only show the best of the two 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
Fri, 16 May 2014 19:13:50 +0200 blanchet use 'simp add:' syntax in Sledgehammer rather than 'using' file | diff | annotate
Thu, 15 May 2014 20:48:13 +0200 blanchet new approach to silence proof methods, to avoid weird theory/context mismatches file | diff | annotate
Tue, 13 May 2014 16:18:16 +0200 blanchet transfer theorems since 'silence_methods' may change the theory file | diff | annotate
Sun, 04 May 2014 21:35:04 +0200 blanchet use right meson tactic for preplaying file | diff | annotate
Sun, 04 May 2014 19:01:36 +0200 blanchet added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0') 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 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
Thu, 13 Feb 2014 13:16:16 +0100 blanchet removed hint that is seldom useful in practice file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed) file | diff | annotate
Tue, 04 Feb 2014 01:35:48 +0100 blanchet removed legacy 'metisFT' method file | diff | annotate
Tue, 04 Feb 2014 01:03:28 +0100 blanchet tuning file | diff | annotate
less more (0) tip
isabelle