--- 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;