--- a/NEWS Thu Jul 28 12:43:50 2005 +0200
+++ b/NEWS Thu Jul 28 15:19:44 2005 +0200
@@ -372,6 +372,9 @@
* Theory Parity: added rules for simplifying exponents.
+* Theories SetsAndFunctions and BigO (see HOL/Library) support
+asymptotic "big O" calculations. See the notes in BigO.thy.
+
*** HOL-Complex ***
@@ -389,12 +392,6 @@
* Theory RComplete: expanded support for floor and ceiling functions.
-*** HOL-Library ***
-
-* Theories SetsAndFunctions and BigO support asymptotic "big O" calculations.
-See the notes in BigO.thy.
-
-
*** HOLCF ***
* HOLCF: discontinued special version of 'constdefs' (which used to