--- a/src/HOL/Auth/Guard/GuardK.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy Thu Sep 28 23:42:35 2006 +0200
@@ -158,9 +158,9 @@
subsection{*set obtained by decrypting a message*}
-syntax decrypt :: "msg set => key => msg => msg set"
-
-translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})"
+abbreviation (input)
+ decrypt :: "msg set => key => msg => msg set"
+ "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 |]
==> Key n:analz (decrypt H K Y)"