src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
Sat, 17 Aug 2013 19:54:16 +0200 wenzelm always enable "minimize" to simplify interaction model;
Sat, 17 Aug 2013 19:13:28 +0200 wenzelm sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
Sat, 17 Aug 2013 12:21:25 +0200 wenzelm eliminated pointless subgoal argument;
Sat, 17 Aug 2013 12:13:53 +0200 wenzelm more direct sledgehammer configuration via mode = Normal_Result and output_result;
Mon, 12 Aug 2013 17:57:51 +0200 wenzelm clarified Query_Operation.register: avoid hard-wired parallel policy;
Thu, 08 Aug 2013 14:24:21 +0200 wenzelm dockable window for Sledgehammer, based on asynchronous/parallel query operation;
Sat, 13 Jul 2013 21:02:41 +0200 wenzelm merged
Sat, 13 Jul 2013 00:50:49 +0200 wenzelm hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
Fri, 12 Jul 2013 23:45:05 +0200 wenzelm system options for Isabelle/HOL proof tools;
Fri, 12 Jul 2013 22:41:25 +0200 smolkas added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
Tue, 09 Jul 2013 18:45:06 +0200 smolkas completely rewrote SH compress; added two parameters for experimentation/fine grained control
Tue, 11 Jun 2013 16:13:19 -0400 smolkas make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
Tue, 21 May 2013 09:02:58 +0200 blanchet added compatibility alias
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer
Wed, 15 May 2013 23:00:17 +0200 wenzelm merged;
Wed, 15 May 2013 22:30:24 +0200 wenzelm clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
Wed, 15 May 2013 20:22:46 +0200 wenzelm maintain ProofGeneral preferences within ProofGeneral module;
Wed, 15 May 2013 17:39:41 +0200 wenzelm just one ProofGeneral module;
Wed, 15 May 2013 17:43:42 +0200 blanchet renamed Sledgehammer functions with 'for' in their names to 'of'
Mon, 06 May 2013 11:03:08 +0200 smolkas added preplay tracing
Wed, 27 Mar 2013 17:58:07 +0100 wenzelm more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
Wed, 20 Feb 2013 14:10:51 +0100 blanchet minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
Wed, 20 Feb 2013 09:58:28 +0100 blanchet fixed typo in option name
Wed, 20 Feb 2013 08:44:24 +0100 blanchet made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
Wed, 20 Feb 2013 08:44:24 +0100 blanchet alias for people like me
Fri, 15 Feb 2013 09:17:26 +0100 blanchet killed legacy alias
Thu, 14 Feb 2013 22:49:22 +0100 smolkas renamed sledgehammer_shrink to sledgehammer_compress
Fri, 11 Jan 2013 14:35:28 +0100 smolkas tuned
Fri, 11 Jan 2013 13:57:51 +0100 smolkas set show_markup to false in order to avoid problems in jedit
Sat, 05 Jan 2013 22:31:30 +0100 blanchet nicer output
Sat, 05 Jan 2013 22:31:30 +0100 blanchet pass option to minimize
Fri, 04 Jan 2013 19:00:49 +0100 blanchet renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
Wed, 19 Dec 2012 22:43:07 +0100 blanchet crank up default timeout for MaSh ATP learning
Sat, 15 Dec 2012 19:57:12 +0100 blanchet thread no timeout properly
Wed, 12 Dec 2012 00:24:06 +0100 blanchet adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
Mon, 12 Nov 2012 14:11:51 +0100 blanchet create temp directory if not already created
Tue, 06 Nov 2012 15:15:33 +0100 blanchet renamed Sledgehammer option
Thu, 18 Oct 2012 15:05:17 +0200 blanchet renamed Isar-proof related options + changed semantics of Isar shrinking
Fri, 28 Sep 2012 09:12:50 +0200 blanchet tuned message
Fri, 14 Sep 2012 12:09:27 +0200 blanchet merged two commands
Thu, 26 Jul 2012 11:07:27 +0200 blanchet detect unknown options again
Mon, 23 Jul 2012 15:32:30 +0200 blanchet don't relearn old facts in Isar mode
Mon, 23 Jul 2012 15:32:30 +0200 blanchet took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
Fri, 20 Jul 2012 22:19:46 +0200 blanchet honor suggested MaSh weights
Fri, 20 Jul 2012 22:19:46 +0200 blanchet use CVC3 and Yices by default if they are available and there are enough cores
Fri, 20 Jul 2012 22:19:46 +0200 blanchet minimal maxes + tuning
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn from SMT proofs when they can be minimized by Metis
Fri, 20 Jul 2012 22:19:46 +0200 blanchet convenience
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learning should honor the fact override and the chained facts
Fri, 20 Jul 2012 22:19:46 +0200 blanchet added "learn_from_atp" command to MaSh, for patient users
Fri, 20 Jul 2012 22:19:46 +0200 blanchet more MaSh docs
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn command in MaSh
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML structures
Wed, 18 Jul 2012 08:44:05 +0200 blanchet optimize parent computation in MaSh + remove temporary files
Wed, 18 Jul 2012 08:44:04 +0200 blanchet learn from minimized ATP proofs
Wed, 18 Jul 2012 08:44:04 +0200 blanchet use async manager to manage MaSh learners to make sure they get killed cleanly
Wed, 18 Jul 2012 08:44:04 +0200 blanchet added option to control which fact filter is used
Wed, 18 Jul 2012 08:44:04 +0200 blanchet make tracing an option
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more implementation work on MaSh
less more (0) -100 -60 tip