# HG changeset patch # User wenzelm # Date 875540368 -7200 # Node ID 9921561ade57437485faede822a18b3d8a17cda1 # Parent fec0f996ae67d2523cd8b4670fdcdd69b48d4ecb tuned; diff -r fec0f996ae67 -r 9921561ade57 NEWS --- a/NEWS Mon Sep 29 15:16:22 1997 +0200 +++ b/NEWS Mon Sep 29 15:39:28 1997 +0200 @@ -7,7 +7,7 @@ *** General Changes *** -* improved output of warnings / errors; +* improved output of warnings (###) / errors (***); * removed old README and Makefiles; @@ -15,7 +15,7 @@ conditional equations; * replaced print_goals_ref hook by print_current_goals_fn and - result_error_fn; +result_error_fn; * removed obsolete init_pps and init_database; @@ -25,9 +25,9 @@ *** Classical Reasoner *** -* Clarify_tac. clarify_tac, clarify_step_tac, Clarify_step_tac : - new tactics that use classical reasoning to simplify a subgoal - without splitting it into several subgoals; +* Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new +tactics that use classical reasoning to simplify a subgoal without +splitting it into several subgoals; * Safe_tac: like safe_tac but uses the default claset; @@ -55,22 +55,23 @@ are rewritten to `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)' -* HOL/Lists: the function "set_of_list" has been renamed "set" (and its - theorems too); +* HOL/Lists: the function "set_of_list" has been renamed "set" (and +its theorems too); *** HOLCF *** * HOLCF: fixed LAM .b syntax (may break some unusual cases); -* added extended adm_tac to simplifier in HOLCF. Can now discharge - adm (%x. P (t x)), where P is chainfinite and t continuous. +* added extended adm_tac to simplifier in HOLCF -- can now discharge +adm (%x. P (t x)), where P is chainfinite and t continuous; *** FOL and ZF *** -* qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available. As - in HOL, they strip ALL and --> from proved theorems; +* qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as +in HOL, they strip ALL and --> from proved theorems; + New in Isabelle94-8 (May 1997)