tuned;
authorwenzelm
Fri Dec 19 10:28:33 1997 +0100 (1997-12-19)
changeset 4449df30e75f670f
parent 4448 b587d40ad474
child 4450 2c64ce912684
tuned;
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/ROOT.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/IMP/ROOT.ML
src/HOL/Induct/ROOT.ML
src/HOL/ex/ROOT.ML
src/HOL/ex/mesontest2.ML
src/HOLCF/ex/ROOT.ML
     1.1 --- a/src/HOL/Auth/NS_Public.ML	Fri Dec 19 10:27:23 1997 +0100
     1.2 +++ b/src/HOL/Auth/NS_Public.ML	Fri Dec 19 10:28:33 1997 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  open NS_Public;
     1.6  
     1.7 -proof_timing:=true;
     1.8 +set proof_timing;
     1.9  HOL_quantifiers := false;
    1.10  
    1.11  AddIffs [Spy_in_bad];
     2.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Fri Dec 19 10:27:23 1997 +0100
     2.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Dec 19 10:28:33 1997 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  open NS_Public_Bad;
     2.6  
     2.7 -proof_timing:=true;
     2.8 +set proof_timing;
     2.9  HOL_quantifiers := false;
    2.10  
    2.11  AddIffs [Spy_in_bad];
     3.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Dec 19 10:27:23 1997 +0100
     3.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Dec 19 10:28:33 1997 +0100
     3.3 @@ -12,7 +12,7 @@
     3.4  
     3.5  open NS_Shared;
     3.6  
     3.7 -proof_timing:=true;
     3.8 +set proof_timing;
     3.9  HOL_quantifiers := false;
    3.10  
    3.11  
     4.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Dec 19 10:27:23 1997 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Dec 19 10:28:33 1997 +0100
     4.3 @@ -14,7 +14,7 @@
     4.4  
     4.5  open OtwayRees;
     4.6  
     4.7 -proof_timing:=true;
     4.8 +set proof_timing;
     4.9  HOL_quantifiers := false;
    4.10  
    4.11  
     5.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 19 10:27:23 1997 +0100
     5.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 19 10:28:33 1997 +0100
     5.3 @@ -14,7 +14,7 @@
     5.4  
     5.5  open OtwayRees_AN;
     5.6  
     5.7 -proof_timing:=true;
     5.8 +set proof_timing;
     5.9  HOL_quantifiers := false;
    5.10  
    5.11  
     6.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Fri Dec 19 10:27:23 1997 +0100
     6.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Dec 19 10:28:33 1997 +0100
     6.3 @@ -17,7 +17,7 @@
     6.4  
     6.5  open OtwayRees_Bad;
     6.6  
     6.7 -proof_timing:=true;
     6.8 +set proof_timing;
     6.9  HOL_quantifiers := false;
    6.10  
    6.11  
     7.1 --- a/src/HOL/Auth/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
     7.2 +++ b/src/HOL/Auth/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
     7.3 @@ -9,7 +9,7 @@
     7.4  HOL_build_completed;    (*Make examples fail if HOL did*)
     7.5  
     7.6  writeln"Root file for HOL/Auth";
     7.7 -proof_timing := true;
     7.8 +set proof_timing;
     7.9  goals_limit := 1;
    7.10  
    7.11  (*Shared-key protocols*)
     8.1 --- a/src/HOL/Auth/Recur.ML	Fri Dec 19 10:27:23 1997 +0100
     8.2 +++ b/src/HOL/Auth/Recur.ML	Fri Dec 19 10:28:33 1997 +0100
     8.3 @@ -8,7 +8,7 @@
     8.4  
     8.5  open Recur;
     8.6  
     8.7 -proof_timing:=true;
     8.8 +set proof_timing;
     8.9  HOL_quantifiers := false;
    8.10  Pretty.setdepth 30;
    8.11  
     9.1 --- a/src/HOL/Auth/TLS.ML	Fri Dec 19 10:27:23 1997 +0100
     9.2 +++ b/src/HOL/Auth/TLS.ML	Fri Dec 19 10:28:33 1997 +0100
     9.3 @@ -19,7 +19,7 @@
     9.4  
     9.5  open TLS;
     9.6  
     9.7 -proof_timing:=true;
     9.8 +set proof_timing;
     9.9  HOL_quantifiers := false;
    9.10  
    9.11  (*Automatically unfold the definition of "certificate"*)
    10.1 --- a/src/HOL/Auth/WooLam.ML	Fri Dec 19 10:27:23 1997 +0100
    10.2 +++ b/src/HOL/Auth/WooLam.ML	Fri Dec 19 10:28:33 1997 +0100
    10.3 @@ -12,7 +12,7 @@
    10.4  
    10.5  open WooLam;
    10.6  
    10.7 -proof_timing:=true;
    10.8 +set proof_timing;
    10.9  HOL_quantifiers := false;
   10.10  
   10.11  
    11.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Dec 19 10:27:23 1997 +0100
    11.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Dec 19 10:28:33 1997 +0100
    11.3 @@ -12,7 +12,7 @@
    11.4  
    11.5  open Yahalom;
    11.6  
    11.7 -proof_timing:=true;
    11.8 +set proof_timing;
    11.9  HOL_quantifiers := false;
   11.10  Pretty.setdepth 25;
   11.11  
    12.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Dec 19 10:27:23 1997 +0100
    12.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Dec 19 10:28:33 1997 +0100
    12.3 @@ -14,7 +14,7 @@
    12.4  
    12.5  open Yahalom2;
    12.6  
    12.7 -proof_timing:=true;
    12.8 +set proof_timing;
    12.9  HOL_quantifiers := false;
   12.10  
   12.11  (*A "possibility property": there are traces that reach the end*)
    13.1 --- a/src/HOL/IMP/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
    13.2 +++ b/src/HOL/IMP/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
    13.3 @@ -7,7 +7,7 @@
    13.4  HOL_build_completed;    (*Make examples fail if HOL did*)
    13.5  
    13.6  writeln"Root file for HOL/IMP";
    13.7 -proof_timing := true;
    13.8 +set proof_timing;
    13.9  time_use_thy "Expr";
   13.10  time_use_thy "Transition";
   13.11  time_use_thy "VC";
    14.1 --- a/src/HOL/Induct/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
    14.2 +++ b/src/HOL/Induct/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
    14.3 @@ -9,7 +9,7 @@
    14.4  HOL_build_completed;    (*Make examples fail if HOL did*)
    14.5  
    14.6  writeln"Root file for HOL/Induct";
    14.7 -proof_timing := true;
    14.8 +set proof_timing;
    14.9  time_use_thy "Perm";
   14.10  time_use_thy "Comb";
   14.11  time_use_thy "Mutil";
    15.1 --- a/src/HOL/ex/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
    15.2 +++ b/src/HOL/ex/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
    15.3 @@ -9,7 +9,7 @@
    15.4  HOL_build_completed;    (*Cause examples to fail if HOL did*)
    15.5  
    15.6  writeln "Root file for HOL examples";
    15.7 -proof_timing := true;
    15.8 +set proof_timing;
    15.9  
   15.10  (**Some examples of recursive function definitions: the TFL package**)
   15.11  time_use_thy "Recdef";
    16.1 --- a/src/HOL/ex/mesontest2.ML	Fri Dec 19 10:27:23 1997 +0100
    16.2 +++ b/src/HOL/ex/mesontest2.ML	Fri Dec 19 10:28:33 1997 +0100
    16.3 @@ -126,7 +126,7 @@
    16.4  
    16.5  val meson_tac = safe_meson_tac 1;
    16.6  
    16.7 -proof_timing:=true;
    16.8 +set proof_timing;
    16.9  
   16.10  (****************ABOVE FIVE MINUTES
   16.11  val BOO003_1 = prove
    17.1 --- a/src/HOLCF/ex/ROOT.ML	Fri Dec 19 10:27:23 1997 +0100
    17.2 +++ b/src/HOLCF/ex/ROOT.ML	Fri Dec 19 10:28:33 1997 +0100
    17.3 @@ -9,7 +9,7 @@
    17.4  HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
    17.5  
    17.6  writeln"Root file for HOLCF examples";
    17.7 -proof_timing := true;
    17.8 +set proof_timing;
    17.9  
   17.10  time_use_thy "Dnat";
   17.11  time_use_thy "Stream";
   17.12 @@ -19,6 +19,3 @@
   17.13  time_use_thy "Hoare";
   17.14  time_use_thy "Loop";
   17.15  time_use "loeckx.ML";
   17.16 -
   17.17 -OS.FileSys.chDir "..";
   17.18 -maketest     "END: Root file for HOLCF examples";