--- a/src/HOL/Auth/Message.thy Tue Jan 07 12:42:48 1997 +0100
+++ b/src/HOL/Auth/Message.thy Tue Jan 07 16:28:43 1997 +0100
@@ -48,7 +48,12 @@
"{|x, y|}" == "MPair x y"
-constdefs (*Keys useful to decrypt elements of a message set*)
+constdefs
+ (*Message Y, paired with a MAC computed with the help of X*)
+ HPair :: "[msg,msg]=>msg"
+ "HPair X Y == {| Hash{|X,Y|}, Y|}"
+
+ (*Keys useful to decrypt elements of a message set*)
keysFor :: msg set => key set
"keysFor H == invKey `` {K. EX X. Crypt K X : H}"