--- a/src/CCL/ex/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/CCL/ex/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -9,12 +9,9 @@
CCL_build_completed; (*Cause examples to fail if CCL did*)
writeln"Root file for CCL examples";
-proof_timing := true;
+set proof_timing;
time_use_thy "Nat";
time_use_thy "List";
time_use_thy "Stream";
time_use_thy "Flag";
-
-OS.FileSys.chDir "..";
-maketest"END: Root file for CCL examples";
--- a/src/CTT/ex/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/CTT/ex/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -11,11 +11,9 @@
CTT_build_completed; (*Cause examples to fail if CTT did*)
print_depth 2;
-proof_timing := true;
+set proof_timing;
+
time_use "typechk.ML";
time_use "elim.ML";
time_use "equal.ML";
time_use "synth.ML";
-
-cd "..";
-maketest"END: Root file for CTT examples";
--- a/src/Cube/ex/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/Cube/ex/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -2,9 +2,6 @@
writeln"Root file for Cube examples";
Cube_build_completed; (*Cause examples to fail if Cube did*)
-proof_timing := true;
+set proof_timing;
-use"ex.ML";
-
-cd "..";
-maketest"END: file for Lambda-Cube examples";
+use "ex.ML";
--- a/src/FOL/ex/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/FOL/ex/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -10,7 +10,7 @@
FOL_build_completed; (*Cause examples to fail if FOL did*)
-proof_timing := true;
+set proof_timing;
time_use "intro.ML";
time_use_thy "Nat";
@@ -39,7 +39,3 @@
writeln"\n** How to declare an oracle **\n";
time_use_thy "IffOracle";
-
-
-OS.FileSys.chDir "..";
-maketest"END: Root file for FOL examples";
--- a/src/FOLP/ex/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/FOLP/ex/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -10,7 +10,7 @@
FOLP_build_completed; (*Cause examples to fail if FOLP did*)
-proof_timing := true;
+set proof_timing;
time_use "intro.ML";
time_use_thy "Nat";
@@ -30,6 +30,3 @@
val thy = FOLP.thy and tac = Cla.fast_tac FOLP_cs 1;
time_use "prop.ML";
time_use "quant.ML";
-
-OS.FileSys.chDir "..";
-maketest"END: Root file for FOLP examples";
--- a/src/LCF/ex/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/LCF/ex/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -2,9 +2,6 @@
writeln"Root file for LCF examples";
LCF_build_completed; (*Cause examples to fail if LCF did*)
-proof_timing := true;
+set proof_timing;
-use"ex.ML";
-
-cd "..";
-maketest"END: file for LCF examples";
+use "ex.ML";
--- a/src/Sequents/ex/ILL/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/Sequents/ex/ILL/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -2,10 +2,9 @@
Sequents_build_completed; (*Cause examples to fail if Sequents did*)
writeln"Root file for ILL examples";
-proof_timing := true;
+set proof_timing;
+
time_use_thy "ILL/washing";
time_use_thy "ILL/ILL_predlog";
time_use "ILL/ILL_kleene_lemmas.ML";
-
-maketest"END: Root file for ILL examples";
--- a/src/Sequents/ex/LK/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/Sequents/ex/LK/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -10,9 +10,7 @@
writeln"Root file for LK examples";
-proof_timing := true;
+set proof_timing;
time_use "LK/prop.ML";
time_use "LK/quant.ML";
time_use "LK/hardquant.ML";
-
-maketest"END: Root file for LK examples";
--- a/src/Sequents/ex/Modal/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/Sequents/ex/Modal/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -6,7 +6,7 @@
Sequents_build_completed; (*Cause examples to fail if Sequents did*)
-proof_timing := true;
+set proof_timing;
writeln "\nTheorems of T\n";
fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
@@ -24,6 +24,3 @@
time_use "Modal/Tthms.ML";
time_use "Modal/S4thms.ML";
time_use "Modal/S43thms.ML";
-
-cd "..";
-maketest"END: Root file for Modal examples";
--- a/src/Sequents/ex/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/Sequents/ex/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -5,6 +5,3 @@
use "LK/ROOT.ML";
use "ILL/ROOT.ML";
use "Modal/ROOT.ML";
-
-OS.FileSys.chDir "..";
-maketest"END: Root file for Sequents examples";
--- a/src/ZF/AC/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/ZF/AC/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -9,7 +9,7 @@
ZF_build_completed; (*Make examples fail if ZF did*)
writeln"Root file for ZF/AC";
-proof_timing := true;
+set proof_timing;
time_use_thy "AC_Equiv";
--- a/src/ZF/Coind/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/ZF/Coind/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -16,6 +16,6 @@
ZF_build_completed; (*Make examples fail if ZF did*)
writeln"Root file for ZF/Coind";
-proof_timing := true;
+set proof_timing;
time_use_thy "MT";
--- a/src/ZF/IMP/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/ZF/IMP/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -15,6 +15,6 @@
ZF_build_completed; (*Make examples fail if ZF did*)
writeln"Root file for ZF/IMP";
-proof_timing := true;
+set proof_timing;
time_use_thy "Equiv";
--- a/src/ZF/Resid/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/ZF/Resid/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -15,7 +15,7 @@
ZF_build_completed; (*Make examples fail if ZF did*)
writeln"Root file for ZF/Resid";
-proof_timing := true;
+set proof_timing;
time_use_thy "Conversion";
--- a/src/ZF/ex/Bin.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/ZF/ex/Bin.ML Fri Dec 19 10:18:03 1997 +0100
@@ -384,7 +384,7 @@
(*** Examples of performing binary arithmetic by simplification ***)
-proof_timing := true;
+set proof_timing;
(*All runtimes below are on a SPARCserver 10*)
goal Bin.thy "#13 $+ #19 = #32";
--- a/src/ZF/ex/ROOT.ML Fri Dec 19 10:17:04 1997 +0100
+++ b/src/ZF/ex/ROOT.ML Fri Dec 19 10:18:03 1997 +0100
@@ -9,7 +9,7 @@
ZF_build_completed; (*Make examples fail if ZF did*)
writeln"Root file for ZF Set Theory examples";
-proof_timing := true;
+set proof_timing;
time_use "misc.ML";
time_use_thy "Primes"; (*GCD theory*)