--- 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*)
--- 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";
--- 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;
--- 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;
--- 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";
--- 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";
--- 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";
--- 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";
--- 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;
--- 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