src/Pure/old_goals.ML
2008-03-26 wenzelm 2008-03-26 moved bind_thm(s) to ML/ml_context.ML; removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);
2008-03-15 wenzelm 2008-03-15 tuned messages;
2007-12-17 wenzelm 2007-12-17 cond_timeit: added message argument;
2007-07-07 wenzelm 2007-07-07 removed obsolete disable_pr/enable_pr; added old print_goals from display.ML;
2007-06-04 wenzelm 2007-06-04 tuned;
2007-04-30 wenzelm 2007-04-30 explicit treatment of legacy_features;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-01-19 wenzelm 2007-01-19 moved inst from drule.ML to old_goals.ML;
2006-10-07 wenzelm 2006-10-07 tuned;
2006-08-03 wenzelm 2006-08-03 removed OldGoals.legacy flag (always warn);
2006-07-27 wenzelm 2006-07-27 Assumption.assume;
2006-02-15 wenzelm 2006-02-15 chop is no longer pervasive; removed obsolete thms_containing;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-11-08 wenzelm 2005-11-08 renamed goals.ML to old_goals.ML; inline Drule.impose_hyps;