--- a/src/HOL/Auth/KerberosV.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/KerberosV.thy Fri Feb 18 15:46:13 2011 +0100
@@ -17,7 +17,7 @@
"Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}