src/Pure/old_goals.ML
2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-12-13 wenzelm 2008-12-13 Context.display_names;
2008-06-23 wenzelm 2008-06-23 Logic.is_all;
2008-06-18 wenzelm 2008-06-18 added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
2008-06-16 wenzelm 2008-06-16 removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm; removed obsolete abbreviations for ML tactic scripts;
2008-06-16 wenzelm 2008-06-16 removed obsolete inst;
2008-06-11 wenzelm 2008-06-11 qualified inst;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-15 wenzelm 2008-04-15 Theory.eq_thy;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 wenzelm 2008-03-27 moved old the_context here; eliminated theory ProtoPure; renamed ML_Context.the_context to ML_Context.the_global_context;
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;