# HG changeset patch
# User wenzelm
# Date 882523083 -3600
# Node ID 097004a470fb5cde2a45cf6ee82ab8273252ce78
# Parent  de74b549f976c066cbf74bbcd0bb7f86587c7b07
tuned;

diff -r de74b549f976 -r 097004a470fb src/CCL/ex/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/CTT/ex/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/Cube/ex/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/FOL/ex/ROOT.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";
diff -r de74b549f976 -r 097004a470fb src/FOLP/ex/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/LCF/ex/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/Sequents/ex/ILL/ROOT.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";
diff -r de74b549f976 -r 097004a470fb src/Sequents/ex/LK/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/Sequents/ex/Modal/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/Sequents/ex/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/ZF/AC/ROOT.ML
--- 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";
 
diff -r de74b549f976 -r 097004a470fb src/ZF/Coind/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/ZF/IMP/ROOT.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/ZF/Resid/ROOT.ML
--- 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";
 
diff -r de74b549f976 -r 097004a470fb src/ZF/ex/Bin.ML
--- 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";
diff -r de74b549f976 -r 097004a470fb src/ZF/ex/ROOT.ML
--- 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*)