2016-04-08 wenzelm 2016-04-08 eliminated ancient TTY-based Tactical.tracify and related global references;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-08-15 wenzelm 2015-08-15 tuned whitespace;
2015-03-09 wenzelm 2015-03-09 support structural composition (THEN_ALL_NEW) for proof methods; clarified preparation for goal restriction: Goal.conjunction_tac only once; export Method.parse0, notably for Eisbach; more explicit type cases_state;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-04-09 wenzelm 2014-04-09 prefer regular Goal_Display.pretty_goals, without censorship of options;
2014-04-09 wenzelm 2014-04-09 proper context for print_tac;
2014-03-20 wenzelm 2014-03-20 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
2013-05-24 wenzelm 2013-05-24 tuned signature;
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-02-15 wenzelm 2012-02-15 eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
2012-02-14 wenzelm 2012-02-14 tuned signature, according to actual usage of these operations;
2012-02-14 wenzelm 2012-02-14 elininated unused INTLEAVE;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2010-09-03 wenzelm 2010-09-03 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-01-13 wenzelm 2010-01-13 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-27 wenzelm 2009-07-27 moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-24 wenzelm 2009-07-24 renamed Pure/tctical.ML to Pure/tactical.ML;