changed use_thy's parameter to exact theory name
authorclasohm
Tue Nov 16 14:10:19 1993 +0100 (1993-11-16)
changeset 121d392174734e9
parent 120 09287f26bfb8
child 122 db9043a8e372
changed use_thy's parameter to exact theory name
src/CCL/ROOT.ML
src/CCL/ex/ROOT.ML
src/CTT/ROOT.ML
src/Cube/ROOT.ML
src/FOL/ROOT.ML
src/FOL/ex/ROOT.ML
src/FOLP/ex/ROOT.ML
src/LCF/ROOT.ML
src/LK/ROOT.ML
src/Modal/ROOT.ML
     1.1 --- a/src/CCL/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     1.2 +++ b/src/CCL/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     1.3 @@ -11,29 +11,27 @@
     1.4  (* Higher-Order Set Theory Extension to FOL *)
     1.5  (*      used as basis for CCL               *)
     1.6  
     1.7 -set_loadpath [".", "../FOL"];
     1.8 -
     1.9 -use_thy "set";
    1.10 +use_thy "Set";
    1.11  use     "subset.ML";
    1.12  use     "equalities.ML";
    1.13  use     "mono.ML";
    1.14 -use_thy "lfp";
    1.15 -use_thy "gfp";
    1.16 +use_thy "Lfp";
    1.17 +use_thy "Gfp";
    1.18  
    1.19  (* CCL - a computational logic for an untyped functional language *)
    1.20  (*                       with evaluation to weak head-normal form *)
    1.21  
    1.22 -use_thy "ccl";
    1.23 -use_thy "term";
    1.24 -use_thy "type";
    1.25 +use_thy "CCL";
    1.26 +use_thy "Term";
    1.27 +use_thy "Type";
    1.28  use     "coinduction.ML";
    1.29 -use_thy "hered";
    1.30 +use_thy "Hered";
    1.31  
    1.32 -use_thy "trancl";
    1.33 -use_thy "wfd";
    1.34 +use_thy "Trancl";
    1.35 +use_thy "Wfd";
    1.36  use     "genrec.ML";
    1.37  use     "typecheck.ML";
    1.38  use     "eval.ML";
    1.39 -use_thy "fix";
    1.40 +use_thy "Fix";
    1.41  
    1.42  val CCL_build_completed = ();   (*indicate successful build*)
     2.1 --- a/src/CCL/ex/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     2.2 +++ b/src/CCL/ex/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     2.3 @@ -10,8 +10,8 @@
     2.4  
     2.5  writeln"Root file for CCL examples";
     2.6  proof_timing := true;
     2.7 -time_use_thy "ex/nat";
     2.8 -time_use_thy "ex/list";
     2.9 -time_use_thy "ex/stream";
    2.10 -time_use_thy "ex/flag";
    2.11 +time_use_thy "ex/Nat";
    2.12 +time_use_thy "ex/List";
    2.13 +time_use_thy "ex/Stream";
    2.14 +time_use_thy "ex/Flag";
    2.15  maketest"END: Root file for CCL examples";
     3.1 --- a/src/CTT/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     3.2 +++ b/src/CTT/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     3.3 @@ -15,11 +15,11 @@
     3.4  structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
     3.5  open Readthy;
     3.6  
     3.7 -use_thy"ctt";
     3.8 +use_thy "CTT";
     3.9  use "../Provers/typedsimp.ML";
    3.10  use "rew.ML";
    3.11 -use_thy "arith";
    3.12 -use_thy "bool";
    3.13 +use_thy "Arith";
    3.14 +use_thy "Bool";
    3.15  
    3.16  use "../Pure/install_pp.ML";
    3.17  print_depth 8;
     4.1 --- a/src/Cube/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     4.2 +++ b/src/Cube/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     4.3 @@ -13,7 +13,7 @@
     4.4  open Readthy;
     4.5  
     4.6  print_depth 1;  
     4.7 -use_thy "cube";
     4.8 +use_thy "Cube";
     4.9  
    4.10  use "../Pure/install_pp.ML";
    4.11  print_depth 8;
     5.1 --- a/src/FOL/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     5.2 +++ b/src/FOL/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     5.3 @@ -15,7 +15,6 @@
     5.4  open Readthy;
     5.5  
     5.6  print_depth 1;  
     5.7 -use_thy "IFOL";
     5.8  use_thy "FOL";
     5.9  
    5.10  use "../Provers/hypsubst.ML";
     6.1 --- a/src/FOL/ex/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     6.2 +++ b/src/FOL/ex/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     6.3 @@ -13,9 +13,9 @@
     6.4  proof_timing := true;
     6.5  
     6.6  time_use     "ex/intro.ML";
     6.7 -time_use_thy "ex/nat";
     6.8 +time_use_thy "ex/Nat";
     6.9  time_use     "ex/foundn.ML";
    6.10 -time_use_thy "ex/prolog";
    6.11 +time_use_thy "ex/Prolog";
    6.12  
    6.13  writeln"\n** Intuitionistic examples **\n";
    6.14  time_use     "ex/int.ML";
    6.15 @@ -26,14 +26,14 @@
    6.16  
    6.17  writeln"\n** Classical examples **\n";
    6.18  time_use     "ex/cla.ML";
    6.19 -time_use_thy "ex/if";
    6.20 +time_use_thy "ex/If";
    6.21  
    6.22  val thy = FOL.thy  and  tac = Cla.fast_tac FOL_cs 1;
    6.23  time_use     "ex/prop.ML";
    6.24  time_use     "ex/quant.ML";
    6.25  
    6.26  writeln"\n** Simplification examples **\n";
    6.27 -time_use_thy "ex/nat2";
    6.28 -time_use_thy "ex/list";
    6.29 +time_use_thy "ex/Nat2";
    6.30 +time_use_thy "ex/List";
    6.31  
    6.32  maketest"END: Root file for FOL examples";
     7.1 --- a/src/FOLP/ex/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     7.2 +++ b/src/FOLP/ex/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     7.3 @@ -11,7 +11,7 @@
     7.4  proof_timing := true;
     7.5  
     7.6  time_use     "ex/intro.ML";
     7.7 -time_use_thy "ex/nat";
     7.8 +time_use_thy "ex/Nat";
     7.9  time_use     "ex/foundn.ML";
    7.10  
    7.11  writeln"\n** Intuitionistic examples **\n";
    7.12 @@ -24,7 +24,7 @@
    7.13  
    7.14  writeln"\n** Classical examples **\n";
    7.15  time_use     "ex/cla.ML";
    7.16 -time_use_thy "ex/if";
    7.17 +time_use_thy "ex/If";
    7.18  
    7.19  val thy = FOLP.thy  and  tac = Cla.fast_tac FOLP_cs 1;
    7.20  time_use     "ex/prop.ML";
     8.1 --- a/src/LCF/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     8.2 +++ b/src/LCF/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     8.3 @@ -11,10 +11,8 @@
     8.4  val banner = "Logic for Computable Functions (in FOL)";
     8.5  writeln banner;
     8.6  
     8.7 -set_loadpath [".", "../FOL"];
     8.8 -
     8.9  print_depth 1;
    8.10 -use_thy "lcf";
    8.11 +use_thy "LCF";
    8.12  use"simpdata.ML";
    8.13  use"pair.ML";
    8.14  use"fix.ML";
     9.1 --- a/src/LK/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     9.2 +++ b/src/LK/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     9.3 @@ -15,7 +15,7 @@
     9.4  
     9.5  print_depth 1;  
     9.6  
     9.7 -use_thy "lk";
     9.8 +use_thy "LK";
     9.9  
    9.10  use "../Pure/install_pp.ML";
    9.11  print_depth 8;
    10.1 --- a/src/Modal/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
    10.2 +++ b/src/Modal/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
    10.3 @@ -7,9 +7,7 @@
    10.4  val banner = "Modal Logic (over LK)";
    10.5  writeln banner;
    10.6  
    10.7 -set_loadpath [".", "../LK"];
    10.8 -
    10.9 -use_thy "modal0";
   10.10 +use_thy "Modal0";
   10.11  
   10.12  structure Modal0_rls = 
   10.13  struct