# HG changeset patch
# User wenzelm
# Date 994191069 -7200
# Node ID d7711be8c3a913c201a8a49d0f741a6028f9bb63
# Parent  0427e3c880628291c806197987f61e5af0a0d34c
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);

diff -r 0427e3c88062 -r d7711be8c3a9 src/HOL/IsaMakefile
--- 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
diff -r 0427e3c88062 -r d7711be8c3a9 src/HOL/Library/Library/ROOT.ML
--- /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";
diff -r 0427e3c88062 -r d7711be8c3a9 src/HOL/Library/ROOT.ML
--- 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";