1.1 --- a/NEWS	Wed Jun 10 11:31:26 2009 +0200
     1.2 +++ b/NEWS	Wed Jun 10 11:31:36 2009 +0200
     1.3 @@ -4,28 +4,38 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Discontinued old form of "escaped symbols" such as \\<forall>.  Only
    1.10 +one backslash should be used, even in ML sources.
    1.11 +
    1.12 +
    1.13  *** Pure ***
    1.14  
    1.15 -* On instantiation of classes, remaining undefined class parameters are
    1.16 -formally declared.  INCOMPATIBILITY.
    1.17 +* On instantiation of classes, remaining undefined class parameters
    1.18 +are formally declared.  INCOMPATIBILITY.
    1.19  
    1.20  
    1.21  *** HOL ***
    1.22  
    1.23 -* Class semiring_div requires superclass no_zero_divisors and proof of div_mult_mult1;
    1.24 -theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
    1.25 -div_mult_mult2 have been generalized to class semiring_div, subsuming former
    1.26 -theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
    1.27 -div_mult_mult1 is now [simp] by default.  INCOMPATIBILITY.
    1.28 -
    1.29 -* Power operations on relations and functions are now one dedicate constant compow with
    1.30 -infix syntax "^^".  Power operations on multiplicative monoids retains syntax "^"
    1.31 -and is now defined generic in class power.  INCOMPATIBILITY.
    1.32 -
    1.33 -* ML antiquotation @{code_datatype} inserts definition of a datatype generated
    1.34 -by the code generator; see Predicate.thy for an example.
    1.35 -
    1.36 -* New method "linarith" invokes existing linear arithmetic decision procedure only.
    1.37 +* Class semiring_div requires superclass no_zero_divisors and proof of
    1.38 +div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
    1.39 +div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
    1.40 +generalized to class semiring_div, subsuming former theorems
    1.41 +zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
    1.42 +zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
    1.43 +INCOMPATIBILITY.
    1.44 +
    1.45 +* Power operations on relations and functions are now one dedicate
    1.46 +constant compow with infix syntax "^^".  Power operations on
    1.47 +multiplicative monoids retains syntax "^" and is now defined generic
    1.48 +in class power.  INCOMPATIBILITY.
    1.49 +
    1.50 +* ML antiquotation @{code_datatype} inserts definition of a datatype
    1.51 +generated by the code generator; see Predicate.thy for an example.
    1.52 +
    1.53 +* New method "linarith" invokes existing linear arithmetic decision
    1.54 +procedure only.
    1.55  
    1.56  
    1.57  *** ML ***