src/Pure/goals.ML
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.
1997-01-17 paulson 1997-01-17 Added the prlim command
1996-11-08 paulson 1996-11-08 Removed "standard" call from uresult, to allow specialist applications
1996-10-24 paulson 1996-10-24 Allowing negative levels (as offsets) in prlev and choplev
1996-08-20 paulson 1996-08-20 Added ref to allow suppression of error msgs
1996-03-28 berghofe 1996-03-28 Added functions pr_latex and printgoal_latex which display current proof state in xdvi window
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-03-11 paulson 1996-03-11 Made an exception handler more specific
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1995-12-22 paulson 1995-12-22 "prepare_proof" has been simplified because rewrite_rule and rewrite_goals_rule check for empty lists. The list of premises is *not* passed to Thm.compress; this was tried, but the potential storage gains seemed not to justify the cpu time required.
1995-09-01 wenzelm 1995-09-01 adapted to new version of shyps-stuff;
1995-08-01 wenzelm 1995-08-01 modified prepare_proof to handle shyps;
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-02-27 lcp 1995-02-27 Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest of the error message ("The exception above was raised for...") will appear. And print_exn calls print_sign_exn_unit so that it can re-raise the SAME exception.