src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots;
Wed, 13 Oct 2021 11:04:35 +0200 wenzelm clarified signature;
Mon, 04 Oct 2021 14:07:15 +0200 wenzelm formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc;
Tue, 28 Sep 2021 10:47:18 +0200 desharna prefer veriT over Z3 in sledgehammer
Tue, 28 Sep 2021 10:38:36 +0200 desharna added Zipperposition to sledgehammer's default provers
Wed, 22 Sep 2021 12:41:40 +0200 desharna removed checks for non-commercial usage of Vampire as it is now under BSD licence
Thu, 08 Jul 2021 17:23:01 +0200 desharna refactored Sledgehammer option "induction_rules"
Thu, 08 Jul 2021 15:25:30 +0200 desharna promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
Fri, 14 May 2021 21:32:11 +0200 wenzelm reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
Thu, 08 Oct 2020 17:02:56 +0200 desharna tune filename
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)
Fri, 25 Oct 2019 14:55:14 +0200 blanchet removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Mon, 02 Jul 2018 10:02:44 +0200 blanchet added option for noncommercial Vampire
Thu, 11 Jan 2018 13:48:17 +0100 wenzelm uniform use of Standard ML op-infix -- eliminated warnings;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Wed, 23 Nov 2016 20:55:58 +0100 blanchet made MaSh faster and less likely to hang seemingly forever
Sun, 14 Aug 2016 12:26:09 +0200 blanchet killed final stops in Sledgehammer and friends
Tue, 24 May 2016 15:24:32 +0200 wenzelm clarified syntax categories;
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Sat, 09 Apr 2016 14:17:50 +0200 wenzelm tuned signature;
Sat, 12 Mar 2016 21:23:58 +0100 wenzelm create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
Fri, 02 Oct 2015 21:15:25 +0200 blanchet further reduced dependency on legacy async thread manager
Fri, 02 Oct 2015 21:06:32 +0200 blanchet removed legacy asynchronous mode in Sledgehammer
Mon, 21 Sep 2015 23:22:11 +0200 wenzelm clarified markup;
Thu, 16 Jul 2015 17:47:49 +0200 blanchet keep smart default for Isar proofs in Sledgehammer panel (if the option is not checked)
Mon, 29 Jun 2015 20:55:46 +0200 wenzelm improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
Thu, 25 Jun 2015 12:41:43 +0200 blanchet put E before (typically remote, hence less reliable) Vampire
Wed, 24 Jun 2015 00:30:03 +0200 blanchet silence 'try'
Thu, 28 May 2015 10:18:46 +0200 blanchet made Auto Sledgehammer behave more like the real thing
Fri, 08 May 2015 15:32:27 +0200 wenzelm sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
Fri, 08 May 2015 15:07:27 +0200 wenzelm more standard command setup;
Sat, 25 Apr 2015 20:49:26 +0200 wenzelm added checkbox for try0;
Wed, 22 Apr 2015 20:14:43 +0200 wenzelm allow diagnostic proof commands with skip_proofs;
Thu, 16 Apr 2015 14:18:32 +0200 wenzelm explicit error for Toplevel.proof_of;
Wed, 08 Apr 2015 18:55:52 +0200 blanchet reorder provers to reflect current eval results
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Wed, 11 Feb 2015 14:48:06 +0100 blanchet tuned default provers
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Fri, 31 Oct 2014 11:18:17 +0100 wenzelm discontinued Proof General;
Thu, 30 Oct 2014 11:08:26 +0100 wenzelm proper syntax categery "name" -- as usual and as documented;
Thu, 28 Aug 2014 20:05:39 +0200 blanchet gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
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.
Thu, 21 Aug 2014 22:48:39 +0200 wenzelm tuned signature -- define some elementary operations earlier;
Mon, 04 Aug 2014 15:02:02 +0200 blanchet cleaner 'compress' option
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
Fri, 01 Aug 2014 14:43:57 +0200 blanchet simplified minimization logic
Wed, 30 Jul 2014 23:52:56 +0200 blanchet always minimize Sledgehammer results by default
Wed, 30 Jul 2014 23:52:56 +0200 blanchet reduced preplay timeout to 1 s
Fri, 25 Jul 2014 13:15:50 +0200 blanchet reordered provers
Sun, 29 Jun 2014 18:28:27 +0200 blanchet compile
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
Wed, 18 Jun 2014 15:23:40 +0200 blanchet more generous formula -- there are lots of duplicates out there
Wed, 18 Jun 2014 14:19:42 +0200 blanchet automatically learn MaSh facts also in 'blocking' mode
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options
Thu, 12 Jun 2014 17:02:03 +0200 blanchet took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
Wed, 11 Jun 2014 11:28:46 +0200 blanchet removed '_new' sufffix in SMT2 solver names (in some cases)
Wed, 11 Jun 2014 11:28:46 +0200 blanchet removed old SMT module from Sledgehammer
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover
Fri, 16 May 2014 19:13:50 +0200 blanchet silence methods even better
Thu, 15 May 2014 20:48:13 +0200 blanchet new approach to silence proof methods, to avoid weird theory/context mismatches
Sun, 04 May 2014 18:14:58 +0200 blanchet improved whitelist (cf. be1874de8344)
Sat, 19 Apr 2014 19:52:02 +0200 wenzelm more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
Tue, 08 Apr 2014 14:59:36 +0200 wenzelm more uniform ML/document antiquotations;
Mon, 31 Mar 2014 10:28:08 +0200 wenzelm support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer
Fri, 14 Feb 2014 10:33:57 +0100 blanchet restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
Thu, 13 Feb 2014 16:21:43 +0100 blanchet do the right thing with provers that exist only remotely (e.g. e_sine)
Mon, 03 Feb 2014 19:32:02 +0100 blanchet renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
Mon, 03 Feb 2014 17:13:31 +0100 blanchet added 'smt' option to control generation of 'by smt' proofs
Mon, 03 Feb 2014 15:33:18 +0100 blanchet tuning
Mon, 03 Feb 2014 10:19:19 +0100 blanchet reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense
Fri, 31 Jan 2014 12:30:54 +0100 blanchet refactor large ML file
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed ML file
Fri, 31 Jan 2014 10:23:32 +0100 blanchet tuned ML file name
less more (0) tip