HOL_quantifiers;
authorwenzelm
Tue Aug 17 22:14:02 1999 +0200 (1999-08-17)
changeset 723926685edee372
parent 7238 36e58620ffc8
child 7240 a509730e424b
HOL_quantifiers;
src/HOL/Auth/KerberosIV.ML
src/HOL/Auth/ROOT.ML
     1.1 --- a/src/HOL/Auth/KerberosIV.ML	Tue Aug 17 22:13:23 1999 +0200
     1.2 +++ b/src/HOL/Auth/KerberosIV.ML	Tue Aug 17 22:14:02 1999 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  
     1.5  Pretty.setdepth 20;
     1.6  proof_timing:=true;
     1.7 -HOL_quantifiers := false;
     1.8  
     1.9  AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];
    1.10  
     2.1 --- a/src/HOL/Auth/ROOT.ML	Tue Aug 17 22:13:23 1999 +0200
     2.2 +++ b/src/HOL/Auth/ROOT.ML	Tue Aug 17 22:14:02 1999 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4  
     2.5  set proof_timing;
     2.6  goals_limit := 1;
     2.7 -HOL_quantifiers := false;
     2.8  
     2.9  (*Shared-key protocols*)
    2.10  time_use_thy "NS_Shared";