src/FOL/ex/ROOT.ML
changeset 121 d392174734e9
parent 0 a5a9c433f639
child 667 661fc2e9c945
     1.1 --- a/src/FOL/ex/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     1.2 +++ b/src/FOL/ex/ROOT.ML	Tue Nov 16 14:10:19 1993 +0100
     1.3 @@ -13,9 +13,9 @@
     1.4  proof_timing := true;
     1.5  
     1.6  time_use     "ex/intro.ML";
     1.7 -time_use_thy "ex/nat";
     1.8 +time_use_thy "ex/Nat";
     1.9  time_use     "ex/foundn.ML";
    1.10 -time_use_thy "ex/prolog";
    1.11 +time_use_thy "ex/Prolog";
    1.12  
    1.13  writeln"\n** Intuitionistic examples **\n";
    1.14  time_use     "ex/int.ML";
    1.15 @@ -26,14 +26,14 @@
    1.16  
    1.17  writeln"\n** Classical examples **\n";
    1.18  time_use     "ex/cla.ML";
    1.19 -time_use_thy "ex/if";
    1.20 +time_use_thy "ex/If";
    1.21  
    1.22  val thy = FOL.thy  and  tac = Cla.fast_tac FOL_cs 1;
    1.23  time_use     "ex/prop.ML";
    1.24  time_use     "ex/quant.ML";
    1.25  
    1.26  writeln"\n** Simplification examples **\n";
    1.27 -time_use_thy "ex/nat2";
    1.28 -time_use_thy "ex/list";
    1.29 +time_use_thy "ex/Nat2";
    1.30 +time_use_thy "ex/List";
    1.31  
    1.32  maketest"END: Root file for FOL examples";