| changeset 21404 | eb85850d3eb7 |
| parent 20768 | 1d478c2d621f |
| child 23746 | a455e69c31cc |
--- a/src/HOL/Auth/Guard/GuardK.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Auth/Guard/GuardK.thy Fri Nov 17 02:20:03 2006 +0100 @@ -159,7 +159,7 @@ subsection{*set obtained by decrypting a message*} abbreviation (input) - decrypt :: "msg set => key => msg => msg set" + decrypt :: "msg set => key => msg => msg set" where "decrypt H K Y == insert Y (H - {Crypt K Y})" lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |]