clarified
authorpaulson
Wed Mar 24 10:55:20 2004 +0100 (2004-03-24)
changeset 1448014b7923b3307
parent 14479 0eca4aabf371
child 14481 ab1e47451aaa
clarified
NEWS
     1.1 --- a/NEWS	Wed Mar 24 10:50:29 2004 +0100
     1.2 +++ b/NEWS	Wed Mar 24 10:55:20 2004 +0100
     1.3 @@ -98,8 +98,9 @@
     1.4      now formalized using the Ring_and_Field theory mentioned above. 
     1.5    - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently
     1.6      than before, because now they are set up once in a generic manner.
     1.7 -  - INCOMPATIBILITY: many type-specific instances of laws proved in 
     1.8 -    Ring_and_Field are no longer available.
     1.9 +  - INCOMPATIBILITY: many type-specific arithmetic laws have gone. 
    1.10 +    Look for the general versions in Ring_and_Field (and Power if they concern
    1.11 +    exponentiation).
    1.12  
    1.13  * Type "rat" of the rational numbers is now available in HOL-Complex.
    1.14