--- 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 <x,y,zs>.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)