src/Pure/goals.ML
2005-10-19 ago removed obsolete old-locales;
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-12 ago introduced new-style AList operations
2005-09-01 ago curried_lookup/update;
2005-08-31 ago refer to theory instead of low-level tsig;
2005-07-13 ago (intermediate commit)
2005-06-20 ago get_thm(s): Name;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-09 ago NameSpace.extern_table;
2005-05-31 ago Sign.declare_name replaces NameSpace.extend;
2005-05-25 ago removed obsolete findI, findE, findEs
2005-05-22 ago findI/Es/E: adapted to FindTheorems.find_XXX, results use thmref instead of string;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-24 ago Adapted to modified interface of PureThy.get_thm(s).
2004-06-09 ago Syntax.default_mode;
2004-05-29 ago Output.timing;
2004-04-22 ago tuned;
2003-02-03 ago Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
2002-11-13 ago Added simple_prove_goal_cterm.
2002-10-21 ago Changed type of Logic.strip_horn.
2002-10-14 ago Ported find_intro/elim to Isar.
2002-07-02 ago emulate old thms_containing;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-09 ago theory data: finish method;
2001-11-01 ago parking code for old-style locales here;
2001-10-27 ago impose hyps on initial goal configuration (prevents res_inst_tac problems);
2001-10-22 ago make this module appeat late in Pure;
2001-09-12 ago result_error_default: include msg;
2001-09-08 ago result_error_default: output *single* error message;
2000-12-29 ago proper error msg;
2000-11-17 ago check result: Envir.beta_norm;
2000-08-10 ago the "nocheck" versions of goal functions now standardize their result
2000-08-04 ago Term.no_dummy_patterns;
2000-05-30 ago global timing flag;
2000-05-18 ago added disable_pr, enable_pr;
2000-01-05 ago TypeInfer.logicT;
1999-10-27 ago reset_goals no longer empties the proof stack
1999-09-29 ago use Drule.strip_shyps_warning;
1999-08-18 ago proper writeln of begin_state;
1999-08-17 ago reset_goals;
1999-07-22 ago avoid '(0 subgoals)';
1999-07-10 ago prove_goalw_cterm_general: pass exeption;
1999-07-07 ago tuned output;
1999-03-17 ago qualify Theory.sign_of etc.;
1999-02-03 ago added Goal(w) and Export (from context.ML);
1999-01-15 ago removed empty line (in case of empty begin_state marker) before Level line
1998-12-04 ago better export for nested locales
1998-11-25 ago removed redirect_to_latex stuff;
1998-10-29 ago tuned current_goals_markers semantics to avoid empty lines;
1998-10-23 ago better reporting of "Additional hypotheses" in a locale
1998-10-22 ago support current_goals_markers ref variable for print_current_goals;
1998-10-05 ago Now prove_goalw_cterm never prints timing statistics
1998-08-13 ago Rule mk_triv_goal for making instances of triv_goal
1998-08-04 ago added export: thm -> thm;
1998-06-29 ago moved actual (C)Pure theories to pure.ML;
1998-06-17 ago Goals may now contain assumptions, which are not returned.
1998-06-05 ago tuned print_exn;