diff -r ad8260dc6e4a -r c20d58286a51 src/HOL/Auth/KerberosIV.ML --- a/src/HOL/Auth/KerberosIV.ML Tue May 30 16:03:09 2000 +0200 +++ b/src/HOL/Auth/KerberosIV.ML Tue May 30 16:08:38 2000 +0200 @@ -7,7 +7,7 @@ *) Pretty.setdepth 20; -proof_timing:=true; +set timing; AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad];