src/Pure/goals.ML
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-06-09 wenzelm 2004-06-09 Syntax.default_mode;
2004-05-29 wenzelm 2004-05-29 Output.timing;
2004-04-22 wenzelm 2004-04-22 tuned;
2003-02-03 berghofe 2003-02-03 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
2002-11-13 berghofe 2002-11-13 Added simple_prove_goal_cterm.
2002-10-21 berghofe 2002-10-21 Changed type of Logic.strip_horn.
2002-10-14 nipkow 2002-10-14 Ported find_intro/elim to Isar.
2002-07-02 wenzelm 2002-07-02 emulate old thms_containing;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-11-01 wenzelm 2001-11-01 parking code for old-style locales here;
2001-10-27 wenzelm 2001-10-27 impose hyps on initial goal configuration (prevents res_inst_tac problems);
2001-10-22 wenzelm 2001-10-22 make this module appeat late in Pure; moved print_current_goals to display.ML; added quick_and_dirty_prove_goalw_cterm (from Isar/skip_proof.ML); added thm database functions (from Thy/thm_database.ML);
2001-09-12 wenzelm 2001-09-12 result_error_default: include msg;
2001-09-08 wenzelm 2001-09-08 result_error_default: output *single* error message;
2000-12-29 wenzelm 2000-12-29 proper error msg;
2000-11-17 wenzelm 2000-11-17 check result: Envir.beta_norm;
2000-08-10 paulson 2000-08-10 the "nocheck" versions of goal functions now standardize their result
2000-08-04 wenzelm 2000-08-04 Term.no_dummy_patterns;
2000-05-30 wenzelm 2000-05-30 global timing flag;
2000-05-18 wenzelm 2000-05-18 added disable_pr, enable_pr;
2000-01-05 wenzelm 2000-01-05 TypeInfer.logicT;
1999-10-27 oheimb 1999-10-27 reset_goals no longer empties the proof stack
1999-09-29 wenzelm 1999-09-29 use Drule.strip_shyps_warning; removed Thm.implies_intr_shyps;
1999-08-18 wenzelm 1999-08-18 proper writeln of begin_state;
1999-08-17 wenzelm 1999-08-17 reset_goals;
1999-07-22 wenzelm 1999-07-22 avoid '(0 subgoals)';
1999-07-10 wenzelm 1999-07-10 prove_goalw_cterm_general: pass exeption;
1999-07-07 wenzelm 1999-07-07 tuned output;
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1999-02-03 wenzelm 1999-02-03 added Goal(w) and Export (from context.ML);
1999-01-15 oheimb 1999-01-15 removed empty line (in case of empty begin_state marker) before Level line added printing of subgoals number in Level line
1998-12-04 paulson 1998-12-04 better export for nested locales
1998-11-25 wenzelm 1998-11-25 removed redirect_to_latex stuff;
1998-10-29 wenzelm 1998-10-29 tuned current_goals_markers semantics to avoid empty lines;
1998-10-23 paulson 1998-10-23 better reporting of "Additional hypotheses" in a locale
1998-10-22 wenzelm 1998-10-22 support current_goals_markers ref variable for print_current_goals;
1998-10-05 paulson 1998-10-05 Now prove_goalw_cterm never prints timing statistics
1998-08-13 paulson 1998-08-13 Rule mk_triv_goal for making instances of triv_goal
1998-08-04 wenzelm 1998-08-04 added export: thm -> thm; exported print_current_goals_default; locale support;
1998-06-29 wenzelm 1998-06-29 moved actual (C)Pure theories to pure.ML;
1998-06-17 nipkow 1998-06-17 Goals may now contain assumptions, which are not returned. This is controlled by an argument `atomic' to the goal commands.
1998-06-05 wenzelm 1998-06-05 tuned print_exn;
1997-11-22 wenzelm 1997-11-22 fixed warning;
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-11-12 wenzelm 1997-11-12 moved 'latex' from library.ML to goals.ML;
1997-10-24 wenzelm 1997-10-24 Pure.thy;
1997-10-23 wenzelm 1997-10-23 Sign.stamp_names_of;
1997-10-13 wenzelm 1997-10-13 uses Sign.str_of_sort;
1997-09-25 paulson 1997-09-25 Prints warnings using the "warning" function instead of "writeln"
1997-09-11 wenzelm 1997-09-11 removed print_goals_ref (which was broken anyway);
1997-07-18 wenzelm 1997-07-18 tuned error propagation msg;
1997-07-18 wenzelm 1997-07-18 tuned warnings; print_current_goals_fn, result_error_fn hooks replace print_goals_ref;
1997-04-16 wenzelm 1997-04-16 Sorts.str_of_sort;
1997-04-02 wenzelm 1997-04-02 changed signature of dummy goal from proto_pure to pure;
1997-02-04 paulson 1997-02-04 Gradual switching to Basis Library functions nth, drop, etc.