src/HOL/Auth/KerberosIV.thy
changeset 35416 d8d7d1b785af
parent 33304 2c77579e0523
child 36866 426d5781bb25
     1.1 --- a/src/HOL/Auth/KerberosIV.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Auth/KerberosIV.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -101,8 +101,7 @@
     1.4  
     1.5  
     1.6  (* Predicate formalising the association between authKeys and servKeys *)
     1.7 -constdefs
     1.8 -  AKcryptSK :: "[key, key, event list] => bool"
     1.9 +definition AKcryptSK :: "[key, key, event list] => bool" where
    1.10    "AKcryptSK authK servK evs ==
    1.11       \<exists>A B Ts.
    1.12         Says Tgs A (Crypt authK