--- a/ROOT.ML Tue Nov 09 16:31:03 1993 +0100
+++ b/ROOT.ML Tue Nov 16 14:14:22 1993 +0100
@@ -15,7 +15,7 @@
print_depth 1;
eta_contract := true;
-use_thy "hol";
+use_thy "HOL";
use "../Provers/hypsubst.ML";
use "../Provers/classical.ML";
use "../Provers/simplifier.ML";
@@ -71,24 +71,24 @@
open HOL_Induction;
use "simpdata.ML";
-use_thy "ord";
-use_thy "set";
+use_thy "Ord";
+use_thy "Set";
use "fun.ML";
use "subset.ML";
use "equalities.ML";
-use_thy "prod";
-use_thy "sum";
+use_thy "Prod";
+use_thy "Sum";
use "mono.ML";
-use_thy "lfp";
-use_thy "gfp";
-use_thy "trancl";
-use_thy "wf";
-use_thy "nat";
-use_thy "arith";
-use_thy "univ";
-use_thy "sexp";
-use_thy "list";
-use_thy "llist";
+use_thy "Lfp";
+use_thy "Gfp";
+use_thy "Trancl";
+use_thy "WF";
+use_thy "Nat";
+use_thy "Arith";
+use_thy "Univ";
+use_thy "Sexp";
+use_thy "List";
+use_thy "LList";
use "../Pure/install_pp.ML";
print_depth 8;
--- a/Subst/ROOT.ML Tue Nov 09 16:31:03 1993 +0100
+++ b/Subst/ROOT.ML Tue Nov 16 14:14:22 1993 +0100
@@ -25,12 +25,12 @@
HOL_build_completed; (*Cause examples to fail if HOL did*)
writeln"Root file for Substitutions and Unification";
-use_thy "Subst/setplus";
+use_thy "Subst/Setplus";
-use_thy "Subst/alist";
-use_thy "Subst/uterm";
-use_thy "Subst/utlemmas";
+use_thy "Subst/AList";
+use_thy "Subst/UTerm";
+use_thy "Subst/UTLemmas";
-use_thy "Subst/subst";
-use_thy "Subst/unifier";
+use_thy "Subst/Subst";
+use_thy "Subst/Unifier";
writeln"END: Root file for Substitutions and Unification";