src/Tools/solve_direct.ML
21 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2017-02-04 wenzelm 2017-02-04 clarified message: print subgoal number instead of potentially large term;
2017-02-04 wenzelm 2017-02-04 tuned;
2017-02-04 wenzelm 2017-02-04 suppress warnings uniformly, even in explicit commands 'find_theorems', 'solve_direct';
2017-02-04 wenzelm 2017-02-04 tuned;
2016-10-03 haftmann 2016-10-03 option to report results of solve_direct as explicit warnings
2016-10-03 haftmann 2016-10-03 modernized option
2016-08-30 blanchet 2016-08-30 tuned final stop in message
2015-04-22 wenzelm 2015-04-22 allow diagnostic proof commands with skip_proofs;
2015-04-16 wenzelm 2015-04-16 explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-11-03 wenzelm 2014-11-03 eliminated obsolete Proof.goal_message -- print outcome more directly;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-10-31 wenzelm 2014-10-31 discontinued Proof General;
2014-04-08 wenzelm 2014-04-08 more uniform ML/document antiquotations;
2013-07-18 wenzelm 2013-07-18 guard unify tracing via visible status of global theory; find_theorems: back-patching of background theory to observe Context_Position.is_visible avoids spamming via auto solve_direct;
2013-07-13 wenzelm 2013-07-13 clarified some default options;
2013-07-13 wenzelm 2013-07-13 more explicit Markup.information for messages produced by "auto" tools;
2013-07-13 wenzelm 2013-07-13 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2013-07-12 wenzelm 2013-07-12 system options for Isabelle/HOL proof tools;
2013-05-15 wenzelm 2013-05-15 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 wenzelm 2013-05-15 maintain ProofGeneral preferences within ProofGeneral module; initialize Isabelle/Pure preferences within normal user space (with antiquotations); tuned;
2013-05-15 wenzelm 2013-05-15 just one ProofGeneral module;
2013-03-27 wenzelm 2013-03-27 more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-14 wenzelm 2012-09-14 clarified markup names;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-05-27 blanchet 2011-05-27 handle non-auto try case gracefully in Solve Direct
2011-05-27 blanchet 2011-05-27 prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
2011-05-27 blanchet 2011-05-27 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-05-27 blanchet 2011-05-27 renamed "Auto_Tools" "Try"
2010-12-03 blanchet 2010-12-03 run synchronous Auto Tools in parallel
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-10-25 wenzelm 2010-10-25 export main ML entry by default; observe elisp format for preferences; clarified command setup;
2010-10-25 wenzelm 2010-10-25 observe Isabelle/ML coding standards;
2010-10-25 blanchet 2010-10-25 introduced manual version of "Auto Solve" as "solve_direct"