diff -r 5396e99c02af -r 492a3d5d2b17 NEWS
--- a/NEWS	Mon May 05 18:50:26 1997 +0200
+++ b/NEWS	Mon May 05 21:18:01 1997 +0200
@@ -33,7 +33,7 @@
 names in bold, underline etc. or colors (which requires a color
 version of xterm);
 
-* now supports alternative (named) syntax tables (parser and pretty
+* supports alternative (named) syntax tables (parser and pretty
 printer); internal interface is provided by add_modesyntax(_i);
 
 * infixes may now be declared with names independent of their syntax;
@@ -54,18 +54,19 @@
     [message "Function Var's argument not a bound variable" relates to this]
   + its proof strategy is more general but can actually be slower
 
-* substitution with equality assumptions no longer permutes other assumptions.
+* substitution with equality assumptions no longer permutes other
+assumptions;
 
 * minor changes in semantics of addafter (now called addaltern); renamed
 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
-(and access functions for it)
+(and access functions for it);
 
 * improved combination of classical reasoner and simplifier: new
 addss, auto_tac, functions for handling clasimpsets, ...  Now, the
 simplification is safe (therefore moved to safe_step_tac) and thus
 more complete, as multiple instantiation of unknowns (with slow_tac).
 COULD MAKE EXISTING PROOFS FAIL; in case of problems with
-old proofs, use unsafe_addss and unsafe_auto_tac
+old proofs, use unsafe_addss and unsafe_auto_tac;
 
 
 *** Simplifier ***
@@ -76,28 +77,29 @@
 
 * ordering on terms as parameter (used for ordered rewriting);
 
-* new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
+* new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
 
 * the solver is now split into a safe and an unsafe part.
 This should be invisible for the normal user, except that the
 functions setsolver and addsolver have been renamed to setSolver and
-addSolver.  added safe_asm_full_simp_tac.
+addSolver; added safe_asm_full_simp_tac;
 
 
 *** HOL ***
 
 * a generic induction tactic `induct_tac' which works for all datatypes and
-also for type `nat'.
+also for type `nat';
 
 * patterns in case expressions allow tuple patterns as arguments to
-constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'
+constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
 
 * primrec now also works with type nat;
 
 * the constant for negation has been renamed from "not" to "Not" to
-harmonize with FOL, ZF, LK, etc.
+harmonize with FOL, ZF, LK, etc.;
 
-* HOL/ex/LFilter theory of a corecursive "filter" functional for infinite lists
+* HOL/ex/LFilter theory of a corecursive "filter" functional for
+infinite lists;
 
 * HOL/ex/Ring.thy declares cring_simp, which solves equational
 problems in commutative rings, using axiomatic type classes for + and *;
@@ -106,6 +108,8 @@
 
 * more default rewrite rules for quantifiers, union/intersection;
 
+* HOLCF/IOA replaces old HOL/IOA;
+
 * HOLCF changes: derived all rules and arities 
   + axiomatic type classes instead of classes 
   + typedef instead of faking type definitions
@@ -114,7 +118,7 @@
   + eliminated the types void, one, tr
   + use unit lift and bool lift (with translations) instead of one and tr
   + eliminated blift from Lift3.thy (use Def instead of blift)
-  all eliminated rules are derived as theorems --> no visible changes 
+  all eliminated rules are derived as theorems --> no visible changes ;
 
 
 *** ZF ***