HOL_quantifiers;
authorwenzelm
Tue, 17 Aug 1999 22:14:02 +0200
changeset 7239 26685edee372
parent 7238 36e58620ffc8
child 7240 a509730e424b
HOL_quantifiers;
src/HOL/Auth/KerberosIV.ML
src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/KerberosIV.ML	Tue Aug 17 22:13:23 1999 +0200
+++ b/src/HOL/Auth/KerberosIV.ML	Tue Aug 17 22:14:02 1999 +0200
@@ -8,7 +8,6 @@
 
 Pretty.setdepth 20;
 proof_timing:=true;
-HOL_quantifiers := false;
 
 AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];
 
--- a/src/HOL/Auth/ROOT.ML	Tue Aug 17 22:13:23 1999 +0200
+++ b/src/HOL/Auth/ROOT.ML	Tue Aug 17 22:14:02 1999 +0200
@@ -10,7 +10,6 @@
 
 set proof_timing;
 goals_limit := 1;
-HOL_quantifiers := false;
 
 (*Shared-key protocols*)
 time_use_thy "NS_Shared";