src/HOL/Auth/KerberosV.thy

--- a/src/HOL/Auth/KerberosV.thy	Fri Apr 02 13:33:48 2010 +0200
+++ b/src/HOL/Auth/KerberosV.thy	Wed Apr 07 19:17:10 2010 +0200
@@ -92,8 +92,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 tt.
        Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, tt\<rbrace>,