diff -r 0eca4aabf371 -r 14b7923b3307 NEWS --- a/NEWS Wed Mar 24 10:50:29 2004 +0100 +++ b/NEWS Wed Mar 24 10:55:20 2004 +0100 @@ -98,8 +98,9 @@ now formalized using the Ring_and_Field theory mentioned above. - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently than before, because now they are set up once in a generic manner. - - INCOMPATIBILITY: many type-specific instances of laws proved in - Ring_and_Field are no longer available. + - INCOMPATIBILITY: many type-specific arithmetic laws have gone. + Look for the general versions in Ring_and_Field (and Power if they concern + exponentiation). * Type "rat" of the rational numbers is now available in HOL-Complex.