src/HOL/Auth/ROOT.ML

 
 writeln"Root file for HOL/Auth";
 
 set proof_timing;
 goals_limit := 1;
-HOL_quantifiers := false;
 
 (*Shared-key protocols*)
 time_use_thy "NS_Shared";
 time_use_thy "Kerberos_BAN";
 time_use_thy "KerberosIV";