src/HOL/Tools/try0.ML
18 months ago blanchet 2017-12-19 have 'try0' display results faster
18 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2016-09-29 boehmes 2016-09-29 invoke argo as part of the tried automatic proof methods
2016-08-14 blanchet 2016-08-14 tuning punctuation in messages output by Isabelle
2016-07-16 wenzelm 2016-07-16 tuned signature;
2016-04-14 wenzelm 2016-04-14 more silence;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2015-12-20 wenzelm 2015-12-20 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-06-01 haftmann 2015-06-01 dropped dead config option
2015-05-08 wenzelm 2015-05-08 silence local Unify.trace_bound as well: existing tools either refer to Proof.context or theory;
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};
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
2014-12-03 wenzelm 2014-12-03 tuned signature;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
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-08-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-08-19 wenzelm 2014-08-19 more compact datatypes;
2014-08-12 wenzelm 2014-08-12 tuned signature according to Scala version -- prefer explicit argument;
2014-05-16 blanchet 2014-05-16 silence methods even better
2014-05-04 blanchet 2014-05-04 added 'satx' proof method to Try0
2014-04-08 wenzelm 2014-04-08 more uniform ML/document antiquotations;
2014-03-10 wenzelm 2014-03-10 clarified Args.check_src: retain name space information for error output; tuned signature;
2014-03-10 wenzelm 2014-03-10 prefer Name_Space.pretty with its builtin markup;
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-02-26 wenzelm 2014-02-26 markup for method combinators;
2014-02-25 wenzelm 2014-02-25 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion; removed obsolete Method.Source_i; proper context for global data; tuned messages;
2014-01-30 blanchet 2014-01-30 more robust w.r.t. exceptions raised by proof methods
2014-01-30 blanchet 2014-01-30 tuning
2014-01-30 blanchet 2014-01-30 tuning
2014-01-30 blanchet 2014-01-30 added 'algebra' and 'meson' to 'try0'
2014-01-30 blanchet 2014-01-30 made 'try0' (more) silent
2013-11-14 blanchet 2013-11-14 made SML/NJ happy
2013-11-08 blanchet 2013-11-08 by (auto ...)[1] not by (auto [1])
2013-11-04 blanchet 2013-11-04 make 'try0' return faster when invoked as part of 'try'
2013-08-17 wenzelm 2013-08-17 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; back to Normal mode: with output_result it is sufficient to determine TTY vs. PIDE operation;
2013-08-12 blanchet 2013-08-12 tuned messages
2013-07-20 wenzelm 2013-07-20 clarified option name, with improved sort order wrt. "time" options;
2013-07-18 wenzelm 2013-07-18 explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
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);
2013-03-09 wenzelm 2013-03-09 tuned;
2012-12-10 wenzelm 2012-12-10 generalized notion of active area, where sendback is just one application; some support for graphview via active area;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-22 wenzelm 2012-11-22 more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e;