# HG changeset patch
# User haftmann
# Date 1258905766 -3600
# Node ID cf8365a709119b317891bc75830ac8f743dc9f11
# Parent  954e8b4ba3d116151809affabbe903c2d648188c
more uniform view on various number theory refinement steps

diff -r 954e8b4ba3d1 -r cf8365a70911 NEWS
--- a/NEWS	Sun Nov 22 15:42:48 2009 +0100
+++ b/NEWS	Sun Nov 22 17:02:46 2009 +0100
@@ -110,31 +110,25 @@
 * ML antiquotation @{code_datatype} inserts definition of a datatype
 generated by the code generator; e.g. see src/HOL/Predicate.thy.
 
-* Combined former theories Divides and IntDiv to one theory Divides in
-the spirit of other number theory theories in HOL; some constants (and
-to a lesser extent also facts) have been suffixed with _nat and _int
-respectively.  INCOMPATIBILITY.
-
 * Most rules produced by inductive and datatype package have mandatory
 prefixes.  INCOMPATIBILITY.
 
 * Reorganization of number theory, INCOMPATIBILITY:
-  - former session NumberTheory now named Old_Number_Theory
-  - new session Number_Theory; prefer this, if possible
-  - moved legacy theories Legacy_GCD and Primes from src/HOL/Library
-    to src/HOL/Old_Number_Theory
+  - new number theory development for nat and int, in
+    theories Divides and GCD as well as in new session
+    Number_Theory
+  - some constants and facts now suffixed with _nat and
+    _int accordingly
+  - former session NumberTheory now named Old_Number_Theory,
+    including theories Legacy_GCD and Primes (prefer Number_Theory
+    if possible)
   - moved theory Pocklington from src/HOL/Library to
     src/HOL/Old_Number_Theory
-  - removed various references to Old_Number_Theory from HOL
-    distribution
 
 * Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
 of finite and infinite sets. It is shown that they form a complete
 lattice.
 
-* Split off prime number ingredients from theory GCD to theory
-Number_Theory/Primes.
-
 * Class semiring_div requires superclass no_zero_divisors and proof of
 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been