--- a/NEWS Tue Sep 01 14:13:34 2009 +0200
+++ b/NEWS Tue Sep 01 15:39:33 2009 +0200
@@ -18,6 +18,15 @@
*** HOL ***
+* Reorganization of number theory:
+ * former session NumberTheory now names Old_Number_Theory; former session NewNumberTheory
+ named NumberTheory;
+ * split off prime number ingredients from theory GCD to theory Number_Theory/Primes;
+ * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/;
+ * moved theory Pocklington from Library/ to Old_Number_Theory/;
+ * removed various references to Old_Number_Theory from HOL distribution.
+INCOMPATIBILITY.
+
* New testing tool "Mirabelle" for automated (proof) tools. Applies
several tools and tactics like sledgehammer, metis, or quickcheck, to
every proof step in a theory. To be used in batch mode via the