arith
authorpaulson
Mon Feb 16 15:24:03 2004 +0100 (2004-02-16)
changeset 1438957c2d90936ba
parent 14388 04f04408b99b
child 14390 55fe71faadda
arith
NEWS
     1.1 --- a/NEWS	Mon Feb 16 03:25:52 2004 +0100
     1.2 +++ b/NEWS	Mon Feb 16 15:24:03 2004 +0100
     1.3 @@ -77,6 +77,19 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, 
     1.8 +    all proved in axiomatic type classes for semirings, rings and fields.
     1.9 +
    1.10 +* Numerics:
    1.11 +  - Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are
    1.12 +    now formalized using the Ring_and_Field theory mentioned above. 
    1.13 +  - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently
    1.14 +    than before, because now they are set up once in a generic manner.
    1.15 +  - INCOMPATIBILITY: many type-specific instances of laws proved in 
    1.16 +    Ring_and_Field are no longer available.
    1.17 +
    1.18 +* Type "rat" of the rational numbers is now availabe in HOL-Complex.
    1.19 +
    1.20  * Records:
    1.21    - Record types are now by default printed with their type abbreviation
    1.22      instead of the list of all field types. This can be configured via