src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
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