src/Tools/try.ML
2014-11-06 wenzelm 2014-11-06 more explicit Keyword.keywords;
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 eliminated odd flags and hook;
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-09-24 wenzelm 2013-09-24 avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-08-10 wenzelm 2013-08-10 explicit "strict" flag for print functions (flipped internal meaning); non-strict query operations may operate on failed states;
2013-08-02 wenzelm 2013-08-02 support print functions with explicit arguments, as provided by overlays;
2013-07-29 wenzelm 2013-07-29 tuned signature;
2013-07-13 wenzelm 2013-07-13 avoid spurious warnings, notably of 'try0' about already declared simps etc.;
2013-07-13 wenzelm 2013-07-13 initial delay for automatically tried tools;
2013-07-13 wenzelm 2013-07-13 tuned;
2013-07-13 wenzelm 2013-07-13 determine print function parameters dynamically, e.g. depending on runtime options;
2013-07-13 wenzelm 2013-07-13 clarified some default options;
2013-07-13 wenzelm 2013-07-13 gutter icon for information messages; avoid redundant Pretty.chunks to keep Markup.information node topmost;
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-04-02 blanchet 2013-04-02 got rid of legacy smartness
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-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-05-30 blanchet 2011-05-30 make SML/NJ happy
2011-05-27 blanchet 2011-05-27 repaired theory merging and defined/used helpers
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 handle non-auto try case of Sledgehammer better
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"