# HG changeset patch
# User wenzelm
# Date 1280847465 -7200
# Node ID 6fda94059baa37663f420d5083f9225282ff45cf
# Parent  bd4965bb7bdc70e1bebd4a80338f70f8f97e4b1f
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);

diff -r bd4965bb7bdc -r 6fda94059baa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Aug 03 16:48:36 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Aug 03 16:57:45 2010 +0200
@@ -395,16 +395,16 @@
 
 HOL-Library: HOL $(OUT)/HOL-Library
 
-$(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML		\
+$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML				\
   $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
   Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
-  Library/AssocList.thy	Library/BigO.thy Library/Binomial.thy		\
+  Library/AssocList.thy Library/BigO.thy Library/Binomial.thy		\
   Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
   Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
-  Library/Code_Integer.thy Library/Code_Natural.thy 			\
+  Library/Code_Integer.thy Library/Code_Natural.thy			\
   Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
   Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
-  Library/Countable.thy	Library/Diagonalize.thy Library/Dlist.thy	\
+  Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
   Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy	\
   Library/Executable_Set.thy Library/Float.thy				\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
@@ -417,15 +417,14 @@
   Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
   Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
   Library/Multiset.thy Library/Nat_Bijection.thy			\
-  Library/Nat_Infinity.thy						\
-  Library/Nested_Environment.thy Library/Numeral_Type.thy		\
-  Library/OptionalSugar.thy Library/Order_Relation.thy			\
-  Library/Permutation.thy Library/Permutations.thy			\
-  Library/Poly_Deriv.thy Library/Polynomial.thy				\
-  Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy		\
-  Library/Product_Vector.thy Library/Product_ord.thy			\
-  Library/Product_plus.thy Library/Quickcheck_Types.thy 		\
-  Library/Quicksort.thy 						\
+  Library/Nat_Infinity.thy Library/Nested_Environment.thy		\
+  Library/Numeral_Type.thy Library/OptionalSugar.thy			\
+  Library/Order_Relation.thy Library/Permutation.thy			\
+  Library/Permutations.thy Library/Poly_Deriv.thy			\
+  Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
+  Library/Preorder.thy Library/Product_Vector.thy			\
+  Library/Product_ord.thy Library/Product_plus.thy			\
+  Library/Quickcheck_Types.thy Library/Quicksort.thy			\
   Library/Quotient_List.thy Library/Quotient_Option.thy			\
   Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
   Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
@@ -440,7 +439,7 @@
   $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
   Library/reflection.ML Library/reify_data.ML				\
   Library/document/root.bib Library/document/root.tex
-	@cd Library; $(ISABELLE_TOOL) usedir -b -f HOL_Library_ROOT.ML $(OUT)/HOL HOL-Library
+	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
 
 
 ## HOL-Hahn_Banach
diff -r bd4965bb7bdc -r 6fda94059baa src/HOL/Library/HOL_Library_ROOT.ML
--- a/src/HOL/Library/HOL_Library_ROOT.ML	Tue Aug 03 16:48:36 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-
-(* Classical Higher-order Logic -- batteries included *)
-
-use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
-  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
diff -r bd4965bb7bdc -r 6fda94059baa src/HOL/Library/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/ROOT.ML	Tue Aug 03 16:57:45 2010 +0200
@@ -0,0 +1,5 @@
+
+(* Classical Higher-order Logic -- batteries included *)
+
+use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
+  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
diff -r bd4965bb7bdc -r 6fda94059baa src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Tue Aug 03 16:48:36 2010 +0200
+++ b/src/HOLCF/IsaMakefile	Tue Aug 03 16:57:45 2010 +0200
@@ -107,8 +107,8 @@
   Library/Strict_Fun.thy \
   Library/Sum_Cpo.thy \
   Library/HOLCF_Library.thy \
-  Library/HOLCF_Library_ROOT.ML
-	@$(ISABELLE_TOOL) usedir -f HOLCF_Library_ROOT.ML $(OUT)/HOLCF Library
+  Library/ROOT.ML
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
 
 
 ## HOLCF-IMP
diff -r bd4965bb7bdc -r 6fda94059baa src/HOLCF/Library/HOLCF_Library_ROOT.ML
--- a/src/HOLCF/Library/HOLCF_Library_ROOT.ML	Tue Aug 03 16:48:36 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thys ["HOLCF_Library"];
diff -r bd4965bb7bdc -r 6fda94059baa src/HOLCF/Library/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Library/ROOT.ML	Tue Aug 03 16:57:45 2010 +0200
@@ -0,0 +1,1 @@
+use_thys ["HOLCF_Library"];