renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
--- 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
--- 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"];
--- /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"];
--- 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
--- 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"];
--- /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"];