--- 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