# HG changeset patch
# User wenzelm
# Date 971904279 -7200
# Node ID 87771e2f49fe4f8ff746aa7b835910a1b8d55edf
# Parent  61824cf550db2217e037c423842a63875428c824
* 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);

diff -r 61824cf550db -r 87771e2f49fe NEWS
--- 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)
 ----------------------------------