src/FOLP/ex/ROOT.ML
changeset 121 d392174734e9
parent 0 a5a9c433f639
child 177 921ad94fdddb
--- 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";