# HG changeset patch
# User wenzelm
# Date 858878885 -3600
# Node ID dd5022d8a5513a16aeda81f2d3fd5ab5290d505f
# Parent  a4f09228b74f7e12cd33fa019c5a9d628f3cc776
exit_use_dir;
tuning;

diff -r a4f09228b74f -r dd5022d8a551 src/Sequents/ex/ILL/ROOT.ML
--- a/src/Sequents/ex/ILL/ROOT.ML	Thu Mar 20 18:27:23 1997 +0100
+++ b/src/Sequents/ex/ILL/ROOT.ML	Thu Mar 20 18:28:05 1997 +0100
@@ -1,12 +1,11 @@
 
-Sequents_build_completed;    (*Cause examples to fail if LK did*)
-
+Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
 writeln"Root file for ILL examples";
 
 proof_timing := true;
-time_use_thy "ex/ILL/washing";
+time_use_thy "ILL/washing";
 
-time_use_thy "ex/ILL/ILL_predlog";
-time_use "ex/ILL/ILL_kleene_lemmas.ML";
+time_use_thy "ILL/ILL_predlog";
+time_use "ILL/ILL_kleene_lemmas.ML";
 
 maketest"END: Root file for ILL examples";
diff -r a4f09228b74f -r dd5022d8a551 src/Sequents/ex/LK/ROOT.ML
--- a/src/Sequents/ex/LK/ROOT.ML	Thu Mar 20 18:27:23 1997 +0100
+++ b/src/Sequents/ex/LK/ROOT.ML	Thu Mar 20 18:28:05 1997 +0100
@@ -6,13 +6,13 @@
 Executes all examples for Classical Logic. 
 *)
 
-Sequents_build_completed;    (*Cause examples to fail if LK did*)
+Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
 
 writeln"Root file for LK examples";
 
 proof_timing := true;
-time_use "ex/LK/prop.ML";
-time_use "ex/LK/quant.ML";
-time_use "ex/LK/hardquant.ML";
+time_use "LK/prop.ML";
+time_use "LK/quant.ML";
+time_use "LK/hardquant.ML";
 
 maketest"END: Root file for LK examples";
diff -r a4f09228b74f -r dd5022d8a551 src/Sequents/ex/Modal/ROOT.ML
--- a/src/Sequents/ex/Modal/ROOT.ML	Thu Mar 20 18:27:23 1997 +0100
+++ b/src/Sequents/ex/Modal/ROOT.ML	Thu Mar 20 18:28:05 1997 +0100
@@ -4,25 +4,26 @@
     Copyright   1991  University of Cambridge
 *)
 
-Sequents_build_completed;    (*Cause examples to fail if Modal did*)
+Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
 
 proof_timing := true;
 
 writeln "\nTheorems of T\n";
 fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
-time_use "ex/Modal/Tthms.ML";
+time_use "Modal/Tthms.ML";
 
 writeln "\nTheorems of S4\n";
 fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
-time_use "ex/Modal/Tthms.ML";
-time_use "ex/Modal/S4thms.ML";
+time_use "Modal/Tthms.ML";
+time_use "Modal/S4thms.ML";
 
 writeln "\nTheorems of S43\n";
 fun try s = (writeln s;
              prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE 
                                            S43_Prover.solve_tac 3]));
-time_use "ex/Modal/Tthms.ML";
-time_use "ex/Modal/S4thms.ML";
-time_use "ex/Modal/S43thms.ML";
+time_use "Modal/Tthms.ML";
+time_use "Modal/S4thms.ML";
+time_use "Modal/S43thms.ML";
 
+cd "..";
 maketest"END: Root file for Modal examples";
diff -r a4f09228b74f -r dd5022d8a551 src/Sequents/ex/ROOT.ML
--- a/src/Sequents/ex/ROOT.ML	Thu Mar 20 18:27:23 1997 +0100
+++ b/src/Sequents/ex/ROOT.ML	Thu Mar 20 18:28:05 1997 +0100
@@ -1,4 +1,10 @@
 
-use "ex/LK/ROOT.ML";
-use "ex/ILL/ROOT.ML";
-use "ex/Modal/ROOT.ML";
+writeln"Root file for Sequents examples";
+Sequents_build_completed;
+
+use "LK/ROOT.ML";
+use "ILL/ROOT.ML";
+use "Modal/ROOT.ML";
+
+OS.FileSys.chDir "..";
+maketest"END: Root file for Sequents examples";