# HG changeset patch
# User wenzelm
# Date 882523713 -3600
# Node ID df30e75f670f46484da0cc54a68312eb1c3ba81e
# Parent  b587d40ad47488eb2118a71e303fb2b1b745cd5a
tuned;

diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -9,7 +9,7 @@
 
 open NS_Public;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 
 AddIffs [Spy_in_bad];
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -13,7 +13,7 @@
 
 open NS_Public_Bad;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 
 AddIffs [Spy_in_bad];
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -12,7 +12,7 @@
 
 open NS_Shared;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 
 
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -14,7 +14,7 @@
 
 open OtwayRees;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 
 
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -14,7 +14,7 @@
 
 open OtwayRees_AN;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 
 
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -17,7 +17,7 @@
 
 open OtwayRees_Bad;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 
 
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -9,7 +9,7 @@
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/Auth";
-proof_timing := true;
+set proof_timing;
 goals_limit := 1;
 
 (*Shared-key protocols*)
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/Recur.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -8,7 +8,7 @@
 
 open Recur;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 Pretty.setdepth 30;
 
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/TLS.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -19,7 +19,7 @@
 
 open TLS;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 
 (*Automatically unfold the definition of "certificate"*)
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/WooLam.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -12,7 +12,7 @@
 
 open WooLam;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 
 
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -12,7 +12,7 @@
 
 open Yahalom;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 Pretty.setdepth 25;
 
diff -r b587d40ad474 -r df30e75f670f src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -14,7 +14,7 @@
 
 open Yahalom2;
 
-proof_timing:=true;
+set proof_timing;
 HOL_quantifiers := false;
 
 (*A "possibility property": there are traces that reach the end*)
diff -r b587d40ad474 -r df30e75f670f src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/IMP/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -7,7 +7,7 @@
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/IMP";
-proof_timing := true;
+set proof_timing;
 time_use_thy "Expr";
 time_use_thy "Transition";
 time_use_thy "VC";
diff -r b587d40ad474 -r df30e75f670f src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/Induct/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -9,7 +9,7 @@
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/Induct";
-proof_timing := true;
+set proof_timing;
 time_use_thy "Perm";
 time_use_thy "Comb";
 time_use_thy "Mutil";
diff -r b587d40ad474 -r df30e75f670f src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -9,7 +9,7 @@
 HOL_build_completed;    (*Cause examples to fail if HOL did*)
 
 writeln "Root file for HOL examples";
-proof_timing := true;
+set proof_timing;
 
 (**Some examples of recursive function definitions: the TFL package**)
 time_use_thy "Recdef";
diff -r b587d40ad474 -r df30e75f670f src/HOL/ex/mesontest2.ML
--- a/src/HOL/ex/mesontest2.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOL/ex/mesontest2.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -126,7 +126,7 @@
 
 val meson_tac = safe_meson_tac 1;
 
-proof_timing:=true;
+set proof_timing;
 
 (****************ABOVE FIVE MINUTES
 val BOO003_1 = prove
diff -r b587d40ad474 -r df30e75f670f src/HOLCF/ex/ROOT.ML
--- a/src/HOLCF/ex/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
+++ b/src/HOLCF/ex/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
@@ -9,7 +9,7 @@
 HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
 
 writeln"Root file for HOLCF examples";
-proof_timing := true;
+set proof_timing;
 
 time_use_thy "Dnat";
 time_use_thy "Stream";
@@ -19,6 +19,3 @@
 time_use_thy "Hoare";
 time_use_thy "Loop";
 time_use "loeckx.ML";
-
-OS.FileSys.chDir "..";
-maketest     "END: Root file for HOLCF examples";