--- 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];
--- 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];
--- 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;
--- 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;
--- 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;
--- 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;
--- 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*)
--- 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;
--- 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"*)
--- 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;
--- 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;
--- 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*)
--- 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";
--- 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";
--- 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";
--- 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
--- 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";