# HG changeset patch
# User wenzelm
# Date 934920842 -7200
# Node ID 26685edee372414136b5b90910fa04d4191a4bac
# Parent  36e58620ffc8352b5cbd12023624f9ec29bf4f18
HOL_quantifiers;

diff -r 36e58620ffc8 -r 26685edee372 src/HOL/Auth/KerberosIV.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];
 
diff -r 36e58620ffc8 -r 26685edee372 src/HOL/Auth/ROOT.ML
--- 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";