src/Provers/blast.ML
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;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 tuned comments;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2007-11-09 wenzelm 2007-11-09 avoid obsolete Sign.read_prop;
2007-08-01 wenzelm 2007-08-01 simplified internal Config interface;
2007-07-31 wenzelm 2007-07-31 replaced depth_limit ref by blast_depth_limit configuration option; tuned method setup;
2007-07-29 wenzelm 2007-07-29 explicit global state argument -- no longer CRITICAL;
2007-07-25 wenzelm 2007-07-25 NAMED_CRITICAL;
2007-07-24 wenzelm 2007-07-24 marked some CRITICAL sections;
2007-07-22 wenzelm 2007-07-22 blast_hyp_subst_tac: plain bool argument;
2007-07-05 wenzelm 2007-07-05 simplified ObjectLogic.atomize;
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 wenzelm 2007-04-04 cleaned-up Output functions;
2006-11-10 wenzelm 2006-11-10 tuned names of start_timing,/end_timing/check_timer;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-04-29 wenzelm 2006-04-29 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-02-14 paulson 2006-02-14 fixed tracing