2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-15 ago less pervasive names from structure Thm;
2010-05-12 ago do not emit legacy_feature warnings here -- users have no chance to disable them;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-27 ago moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
2010-03-07 ago modernized structure Object_Logic;
2010-02-19 ago moved ancient Drule.get_def to OldGoals.get_def;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-21 ago removed old-style \ and \\ infixes
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-10-17 ago explicitly qualify Drule.standard;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-28 ago modernized messages -- eliminated ctyp/cterm operations;
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;