| changeset 41774 | 13b97824aec6 |
| parent 37936 | 1e4c5015a72e |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Auth/KerberosIV_Gets.thy Fri Feb 18 15:17:39 2011 +0100 +++ b/src/HOL/Auth/KerberosIV_Gets.thy Fri Feb 18 15:46:13 2011 +0100 @@ -16,7 +16,7 @@ Tgs :: agent where "Tgs == Friend 0" -axioms +axiomatization where Tgs_not_bad [iff]: "Tgs \<notin> bad" --{*Tgs is secure --- we already know that Kas is secure*}