src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2013-11-21 ago fixed spying so that the envirnoment variables are queried at run-time not at build-time
2013-11-19 ago tuning
2013-10-17 ago added comment
2013-10-15 ago use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
2013-10-04 ago run fewer provers in "try" mode
2013-10-04 ago count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)
2013-09-23 ago added "spy" option to Sledgehammer
2013-09-20 ago merged "isar_try0" and "isar_minimize" options
2013-09-20 ago hardcoded obscure option
2013-09-20 ago hard-coded an obscure option
2013-09-20 ago use configuration mechanism for low-level tracing
2013-09-20 ago took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
2013-09-20 ago tuning (use a blacklist instead of a whitelist)
2013-08-22 ago fixed subtle bug with "take" + thread overlord through
2013-08-22 ago have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
2013-08-17 ago prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
2013-08-17 ago some protocol to determine provers according to ML;
2013-08-17 ago always enable "minimize" to simplify interaction model;
2013-08-17 ago 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;
2013-08-17 ago eliminated pointless subgoal argument;
2013-08-17 ago more direct sledgehammer configuration via mode = Normal_Result and output_result;
2013-08-12 ago clarified Query_Operation.register: avoid hard-wired parallel policy;
2013-08-08 ago dockable window for Sledgehammer, based on asynchronous/parallel query operation;
2013-07-13 ago merged
2013-07-13 ago hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2013-07-12 ago system options for Isabelle/HOL proof tools;
2013-07-12 ago added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
2013-07-09 ago completely rewrote SH compress; added two parameters for experimentation/fine grained control
2013-06-11 ago make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
2013-05-21 ago added compatibility alias
2013-05-16 ago tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-15 ago merged;
2013-05-15 ago clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
2013-05-15 ago maintain ProofGeneral preferences within ProofGeneral module;
2013-05-15 ago just one ProofGeneral module;
2013-05-15 ago renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-06 ago added preplay tracing
2013-03-27 ago more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
2013-02-20 ago minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
2013-02-20 ago fixed typo in option name
2013-02-20 ago made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
2013-02-20 ago alias for people like me
2013-02-15 ago killed legacy alias
2013-02-14 ago renamed sledgehammer_shrink to sledgehammer_compress
2013-01-11 ago tuned
2013-01-11 ago set show_markup to false in order to avoid problems in jedit
2013-01-05 ago nicer output
2013-01-05 ago pass option to minimize
2013-01-04 ago renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
2012-12-19 ago crank up default timeout for MaSh ATP learning
2012-12-15 ago thread no timeout properly
2012-12-12 ago adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
2012-11-12 ago create temp directory if not already created
2012-11-06 ago renamed Sledgehammer option
2012-10-18 ago renamed Isar-proof related options + changed semantics of Isar shrinking
2012-09-28 ago tuned message
2012-09-14 ago merged two commands
2012-07-26 ago detect unknown options again
2012-07-23 ago don't relearn old facts in Isar mode
2012-07-23 ago took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks