* HOL/Library: a collection of generic theories to be used together
with main HOL; the theory loader path already includes this directory
by default; the following existing theories have been moved here:
HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
(as While_Combinator);

--- a/NEWS	Wed Oct 18 17:47:01 2000 +0200
+++ b/NEWS	Wed Oct 18 23:24:39 2000 +0200
@@ -1,3 +1,4 @@
+
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -6,6 +7,22 @@
 * HOL: induct renamed to lfp_induct;
 
 
+*** Document preparation ***
+
+* improved isabelle style files; more abstract symbol implementation
+(should now use \isamath{...} and \isatext{...} in custom symbol
+definitions);
+
+
+*** HOL ***
+
+* HOL/Library: a collection of generic theories to be used together
+with main HOL; the theory loader path already includes this directory
+by default; the following existing theories have been moved here:
+HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
+(as While_Combinator);
+
+
 New in Isabelle99-1 (October 2000)
 ----------------------------------