src/FOLP/ex/ROOT.ML
changeset 1351 4a960c012383
parent 1296 ae31bb7774a7
child 1459 d12da312eff4
--- a/src/FOLP/ex/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/FOLP/ex/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -12,26 +12,25 @@
 
 proof_timing := true;
 
-time_use     "ex/intro.ML";
-time_use_thy "ex/Nat";
-time_use     "ex/foundn.ML";
+time_use     "intro.ML";
+time_use_thy "Nat";
+time_use     "foundn.ML";
 
 writeln"\n** Intuitionistic examples **\n";
-time_use     "ex/int.ML";
+time_use     "int.ML";
 
 val thy = IFOLP.thy  and  tac = Int.fast_tac 1;
-time_use     "ex/prop.ML";
-time_use     "ex/quant.ML";
+time_use     "prop.ML";
+time_use     "quant.ML";
 commit();
 
 writeln"\n** Classical examples **\n";
-time_use     "ex/cla.ML";
-time_use_thy "ex/If";
+time_use     "cla.ML";
+time_use_thy "If";
 
 val thy = FOLP.thy  and  tac = Cla.fast_tac FOLP_cs 1;
-time_use     "ex/prop.ML";
-time_use     "ex/quant.ML";
+time_use     "prop.ML";
+time_use     "quant.ML";
 
-make_chart ();   (*make HTML chart*)
-
+cd "..";
 maketest"END: Root file for FOLP examples";