src/Provers/blast.ML
2016-06-10 paulson 2016-06-10 code to catch exception TERM in blast
2016-06-10 paulson 2016-06-10 Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
2015-10-12 wenzelm 2015-10-12 proper message;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-08-16 wenzelm 2015-08-16 tuned signature;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context;
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-01-07 wenzelm 2014-01-07 avoid hard tabs in output -- somewhat ill-defined;
2014-01-07 wenzelm 2014-01-07 uniform output of tracing via official channel (usually depending on trace flag); warning subject to context visibility;
2014-01-01 wenzelm 2014-01-01 clarified blast after change of SELECT_GOAL in 210bca64b894: do not smash flex-flex pairs of overall goal state (in analogy to maxidx) -- NB: Isar goal structure serves as natural boundary, e.g. in "by blast";
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-09-11 wenzelm 2013-09-11 do not expose internal flags to attribute name space;
2012-02-27 wenzelm 2012-02-27 tuned;
2011-06-10 wenzelm 2011-06-10 local gensym based on Name.variant; do not export internals by default;
2011-06-10 wenzelm 2011-06-10 uniform use of flexflex_rule;
2011-06-10 wenzelm 2011-06-10 more official options blast_trace, blast_stats;
2011-06-09 wenzelm 2011-06-09 clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b); uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac; tuned blast_tac: atomize prems only once, outside DEEPEN;
2011-05-30 paulson 2011-05-30 Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
2011-05-15 wenzelm 2011-05-15 tuned signature;
2011-05-14 wenzelm 2011-05-14 eliminated global Unsynchronized.ref; eliminated Display.string_of_thm_without_context;
2011-05-14 wenzelm 2011-05-14 simplified BLAST_DATA;
2011-05-14 wenzelm 2011-05-14 proper Proof.context -- eliminated global operations;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-26 wenzelm 2011-04-26 simplified Blast setup;
2011-04-16 wenzelm 2011-04-16 tuned blast: navigate to subgoal only once;
2011-04-16 wenzelm 2011-04-16 more direct Thm.cprem_of (with exception THM instead of Subscript);
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-10 wenzelm 2010-05-10 renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-03-28 wenzelm 2010-03-28 static defaults for configuration options;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-24 wenzelm 2009-07-24 renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;
2009-07-24 wenzelm 2009-07-24 explicit OldGoals;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-17 wenzelm 2009-03-17 renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
2009-03-15 wenzelm 2009-03-15 simplified method setup;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-06 wenzelm 2009-03-06 eliminated Output.immediate_output -- violates the official message channel protocol;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-03-01 wenzelm 2009-03-01 end_timing: generalized result -- message plus with explicit time values;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;