NEWS
changeset 3744 9921561ade57
parent 3719 6a142dab2a08
child 3822 a17f9b8dca93
--- 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)