src/Pure/tactical.ML
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;