Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
uses of this ML file (HOL/Library is in the default load path);

--- a/src/HOL/IsaMakefile	Tue Jul 03 15:40:25 2001 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 03 22:11:09 2001 +0200
@@ -187,9 +187,9 @@
   Library/Quotient.thy Library/Ring_and_Field.thy \
   Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
   Library/README.html Library/Continuity.thy \
-  Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \
-  Library/While_Combinator.thy
-	@$(ISATOOL) usedir $(OUT)/HOL Library
+  Library/Nested_Environment.thy Library/Rational_Numbers.thy \
+  Library/Library/ROOT.ML Library/While_Combinator.thy
+	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
 
 
 ## HOL-Subst

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Library/ROOT.ML	Tue Jul 03 22:11:09 2001 +0200
@@ -0,0 +1,1 @@
+use_thy "Library";

--- a/src/HOL/Library/ROOT.ML	Tue Jul 03 15:40:25 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thy "Library";