src/HOL/Auth/KerberosIV.thy

--- a/src/HOL/Auth/KerberosIV.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Auth/KerberosIV.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -101,8 +101,7 @@
 
 
 (* Predicate formalising the association between authKeys and servKeys *)
-constdefs
-  AKcryptSK :: "[key, key, event list] => bool"
+definition AKcryptSK :: "[key, key, event list] => bool" where
   "AKcryptSK authK servK evs ==
      \<exists>A B Ts.
        Says Tgs A (Crypt authK