diff -r d58d6acab331 -r 398c0f48a99e NEWS
--- a/NEWS	Wed Jun 10 11:31:26 2009 +0200
+++ b/NEWS	Wed Jun 10 11:31:36 2009 +0200
@@ -4,28 +4,38 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Discontinued old form of "escaped symbols" such as \\<forall>.  Only
+one backslash should be used, even in ML sources.
+
+
 *** Pure ***
 
-* On instantiation of classes, remaining undefined class parameters are
-formally declared.  INCOMPATIBILITY.
+* On instantiation of classes, remaining undefined class parameters
+are formally declared.  INCOMPATIBILITY.
 
 
 *** HOL ***
 
-* Class semiring_div requires superclass no_zero_divisors and proof of div_mult_mult1;
-theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
-div_mult_mult2 have been generalized to class semiring_div, subsuming former
-theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
-div_mult_mult1 is now [simp] by default.  INCOMPATIBILITY.
-
-* Power operations on relations and functions are now one dedicate constant compow with
-infix syntax "^^".  Power operations on multiplicative monoids retains syntax "^"
-and is now defined generic in class power.  INCOMPATIBILITY.
-
-* ML antiquotation @{code_datatype} inserts definition of a datatype generated
-by the code generator; see Predicate.thy for an example.
-
-* New method "linarith" invokes existing linear arithmetic decision procedure only.
+* Class semiring_div requires superclass no_zero_divisors and proof of
+div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
+div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
+generalized to class semiring_div, subsuming former theorems
+zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
+zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
+INCOMPATIBILITY.
+
+* Power operations on relations and functions are now one dedicate
+constant compow with infix syntax "^^".  Power operations on
+multiplicative monoids retains syntax "^" and is now defined generic
+in class power.  INCOMPATIBILITY.
+
+* ML antiquotation @{code_datatype} inserts definition of a datatype
+generated by the code generator; see Predicate.thy for an example.
+
+* New method "linarith" invokes existing linear arithmetic decision
+procedure only.
 
 
 *** ML ***