# HG changeset patch
# User clasohm
# Date 753455419 -3600
# Node ID d392174734e9e6237991f895bae924f3ef361d50
# Parent  09287f26bfb8bc5105ef0e52475a10082b7436b5
changed use_thy's parameter to exact theory name

diff -r 09287f26bfb8 -r d392174734e9 src/CCL/ROOT.ML
--- a/src/CCL/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/CCL/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -11,29 +11,27 @@
 (* Higher-Order Set Theory Extension to FOL *)
 (*      used as basis for CCL               *)
 
-set_loadpath [".", "../FOL"];
-
-use_thy "set";
+use_thy "Set";
 use     "subset.ML";
 use     "equalities.ML";
 use     "mono.ML";
-use_thy "lfp";
-use_thy "gfp";
+use_thy "Lfp";
+use_thy "Gfp";
 
 (* CCL - a computational logic for an untyped functional language *)
 (*                       with evaluation to weak head-normal form *)
 
-use_thy "ccl";
-use_thy "term";
-use_thy "type";
+use_thy "CCL";
+use_thy "Term";
+use_thy "Type";
 use     "coinduction.ML";
-use_thy "hered";
+use_thy "Hered";
 
-use_thy "trancl";
-use_thy "wfd";
+use_thy "Trancl";
+use_thy "Wfd";
 use     "genrec.ML";
 use     "typecheck.ML";
 use     "eval.ML";
-use_thy "fix";
+use_thy "Fix";
 
 val CCL_build_completed = ();   (*indicate successful build*)
diff -r 09287f26bfb8 -r d392174734e9 src/CCL/ex/ROOT.ML
--- a/src/CCL/ex/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/CCL/ex/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -10,8 +10,8 @@
 
 writeln"Root file for CCL examples";
 proof_timing := true;
-time_use_thy "ex/nat";
-time_use_thy "ex/list";
-time_use_thy "ex/stream";
-time_use_thy "ex/flag";
+time_use_thy "ex/Nat";
+time_use_thy "ex/List";
+time_use_thy "ex/Stream";
+time_use_thy "ex/Flag";
 maketest"END: Root file for CCL examples";
diff -r 09287f26bfb8 -r d392174734e9 src/CTT/ROOT.ML
--- a/src/CTT/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/CTT/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -15,11 +15,11 @@
 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
 open Readthy;
 
-use_thy"ctt";
+use_thy "CTT";
 use "../Provers/typedsimp.ML";
 use "rew.ML";
-use_thy "arith";
-use_thy "bool";
+use_thy "Arith";
+use_thy "Bool";
 
 use "../Pure/install_pp.ML";
 print_depth 8;
diff -r 09287f26bfb8 -r d392174734e9 src/Cube/ROOT.ML
--- a/src/Cube/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/Cube/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -13,7 +13,7 @@
 open Readthy;
 
 print_depth 1;  
-use_thy "cube";
+use_thy "Cube";
 
 use "../Pure/install_pp.ML";
 print_depth 8;
diff -r 09287f26bfb8 -r d392174734e9 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/FOL/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -15,7 +15,6 @@
 open Readthy;
 
 print_depth 1;  
-use_thy "IFOL";
 use_thy "FOL";
 
 use "../Provers/hypsubst.ML";
diff -r 09287f26bfb8 -r d392174734e9 src/FOL/ex/ROOT.ML
--- a/src/FOL/ex/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/FOL/ex/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -13,9 +13,9 @@
 proof_timing := true;
 
 time_use     "ex/intro.ML";
-time_use_thy "ex/nat";
+time_use_thy "ex/Nat";
 time_use     "ex/foundn.ML";
-time_use_thy "ex/prolog";
+time_use_thy "ex/Prolog";
 
 writeln"\n** Intuitionistic examples **\n";
 time_use     "ex/int.ML";
@@ -26,14 +26,14 @@
 
 writeln"\n** Classical examples **\n";
 time_use     "ex/cla.ML";
-time_use_thy "ex/if";
+time_use_thy "ex/If";
 
 val thy = FOL.thy  and  tac = Cla.fast_tac FOL_cs 1;
 time_use     "ex/prop.ML";
 time_use     "ex/quant.ML";
 
 writeln"\n** Simplification examples **\n";
-time_use_thy "ex/nat2";
-time_use_thy "ex/list";
+time_use_thy "ex/Nat2";
+time_use_thy "ex/List";
 
 maketest"END: Root file for FOL examples";
diff -r 09287f26bfb8 -r d392174734e9 src/FOLP/ex/ROOT.ML
--- a/src/FOLP/ex/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/FOLP/ex/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -11,7 +11,7 @@
 proof_timing := true;
 
 time_use     "ex/intro.ML";
-time_use_thy "ex/nat";
+time_use_thy "ex/Nat";
 time_use     "ex/foundn.ML";
 
 writeln"\n** Intuitionistic examples **\n";
@@ -24,7 +24,7 @@
 
 writeln"\n** Classical examples **\n";
 time_use     "ex/cla.ML";
-time_use_thy "ex/if";
+time_use_thy "ex/If";
 
 val thy = FOLP.thy  and  tac = Cla.fast_tac FOLP_cs 1;
 time_use     "ex/prop.ML";
diff -r 09287f26bfb8 -r d392174734e9 src/LCF/ROOT.ML
--- a/src/LCF/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/LCF/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -11,10 +11,8 @@
 val banner = "Logic for Computable Functions (in FOL)";
 writeln banner;
 
-set_loadpath [".", "../FOL"];
-
 print_depth 1;
-use_thy "lcf";
+use_thy "LCF";
 use"simpdata.ML";
 use"pair.ML";
 use"fix.ML";
diff -r 09287f26bfb8 -r d392174734e9 src/LK/ROOT.ML
--- a/src/LK/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/LK/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -15,7 +15,7 @@
 
 print_depth 1;  
 
-use_thy "lk";
+use_thy "LK";
 
 use "../Pure/install_pp.ML";
 print_depth 8;
diff -r 09287f26bfb8 -r d392174734e9 src/Modal/ROOT.ML
--- a/src/Modal/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
+++ b/src/Modal/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
@@ -7,9 +7,7 @@
 val banner = "Modal Logic (over LK)";
 writeln banner;
 
-set_loadpath [".", "../LK"];
-
-use_thy "modal0";
+use_thy "Modal0";
 
 structure Modal0_rls = 
 struct