diff -r 70479ec9f44f -r 1c3327c348b3 NEWS
--- a/NEWS	Fri Aug 02 11:12:34 2002 +0200
+++ b/NEWS	Fri Aug 02 11:49:55 2002 +0200
@@ -28,16 +28,23 @@
 
 *** HOL ***
 
-* attribute [symmetric] now works for relations as well. It turns
-  (x,y) : R^-1 into (y,x) : R, and vice versa.
-
-* arith(_tac) does now know about div k and mod k where k is a numeral of
-  type nat or int. It can solve simple goals like
+* 'typedef' command has new option "open" to suppress the set
+definition;
+
+* attribute [symmetric] now works for relations as well; it turns
+(x,y) : R^-1 into (y,x) : R, and vice versa;
+
+* arith(_tac) does now know about div k and mod k where k is a numeral
+of type nat or int. It can solve simple goals like
+
   "0 < n ==> n div 2 < (n::nat)"
-  but fails if divisibility plays a role like in
-  "n div 2 + (n+1) div 2 = (n::nat)".
-* simp's arithmetic capabilities have been enhanced a bit:
-  it now takes ~= in premises into account (by performing a case split).
+
+but fails if divisibility plays a role like in
+
+  "n div 2 + (n+1) div 2 = (n::nat)"
+
+* simp's arithmetic capabilities have been enhanced a bit: it now
+takes ~= in premises into account (by performing a case split);