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;