# HG changeset patch
# User paulson
# Date 1076941443 -3600
# Node ID 57c2d90936ba7bdf8cb62a5269e0c3bb3be2b4e3
# Parent  04f04408b99be6b1aba6fd8b1e0542de9f26a182
arith

diff -r 04f04408b99b -r 57c2d90936ba NEWS
--- a/NEWS	Mon Feb 16 03:25:52 2004 +0100
+++ b/NEWS	Mon Feb 16 15:24:03 2004 +0100
@@ -77,6 +77,19 @@
 
 *** HOL ***
 
+* Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, 
+    all proved in axiomatic type classes for semirings, rings and fields.
+
+* Numerics:
+  - Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are
+    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.
+
+* Type "rat" of the rational numbers is now availabe in HOL-Complex.
+
 * Records:
   - Record types are now by default printed with their type abbreviation
     instead of the list of all field types. This can be configured via