--- a/NEWS Sun Sep 18 15:39:55 2011 +0200
+++ b/NEWS Sun Sep 18 15:57:36 2011 +0200
@@ -304,8 +304,9 @@
reals found in probability theory. This file is extended by
Multivariate_Analysis/Extended_Real_Limits.
-* Old 'recdef' package has been moved to theory Library/Old_Recdef,
-from where it must be imported explicitly. INCOMPATIBILITY.
+* Theory Library/Old_Recdef: old 'recdef' package has been moved here,
+from where it must be imported explicitly if it is really required.
+INCOMPATIBILITY.
* Theory Library/Wfrec: well-founded recursion combinator "wfrec" has
been moved here. INCOMPATIBILITY.