src/Pure/old_goals.ML
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 eliminated the_context;
2009-07-24 ago structure OldGoals: no pervasive names;
2009-07-23 ago clarified pretty_goals, pretty_thm_aux: plain context;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-20 ago moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
2009-01-21 ago removed Ids;
2008-12-13 ago Context.display_names;
2008-06-23 ago Logic.is_all;
2008-06-18 ago added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
2008-06-16 ago removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm;
2008-06-16 ago removed obsolete inst;
2008-06-11 ago qualified inst;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago structure Display: less pervasive operations;
2008-04-15 ago Theory.eq_thy;
2008-04-15 ago Thm.forall_elim_var(s);
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 ago moved old the_context here;
2008-03-26 ago moved bind_thm(s) to ML/ml_context.ML;
2008-03-15 ago tuned messages;
2007-12-17 ago cond_timeit: added message argument;
2007-07-07 ago removed obsolete disable_pr/enable_pr;
2007-06-04 ago tuned;
2007-04-30 ago explicit treatment of legacy_features;
2007-04-14 ago cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-01-19 ago moved inst from drule.ML to old_goals.ML;
2006-10-07 ago tuned;
2006-08-03 ago removed OldGoals.legacy flag (always warn);
2006-07-27 ago Assumption.assume;
2006-02-15 ago chop is no longer pervasive;
2006-01-14 ago sane ERROR handling;
2005-11-08 ago renamed goals.ML to old_goals.ML;