src/HOL/Auth/TLS.ML
changeset 4449 df30e75f670f
parent 4423 a129b817b58a
child 4472 cfa3bd184bc1
equal deleted inserted replaced
4448:b587d40ad474 4449:df30e75f670f
    17   rollback attacks).
    17   rollback attacks).
    18 *)
    18 *)
    19 
    19 
    20 open TLS;
    20 open TLS;
    21 
    21 
    22 proof_timing:=true;
    22 set proof_timing;
    23 HOL_quantifiers := false;
    23 HOL_quantifiers := false;
    24 
    24 
    25 (*Automatically unfold the definition of "certificate"*)
    25 (*Automatically unfold the definition of "certificate"*)
    26 Addsimps [certificate_def];
    26 Addsimps [certificate_def];
    27 
    27