2012-10-16 ago clarified defer/prefer: more specific errors;
2012-02-15 ago eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
2012-02-14 ago tuned signature, according to actual usage of these operations;
2012-02-14 ago elininated unused INTLEAVE;
2011-06-08 ago more robust exception pattern General.Subscript;
2010-09-03 ago 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 ago 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 ago explicit indication of Unsynchronized.ref;
2009-07-27 ago moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-25 ago renamed structure Display_Goal to Goal_Display;
2009-07-24 ago renamed Pure/tctical.ML to Pure/tactical.ML;