diff -r 95c2f9c0930a -r 596a5b5a68ff src/HOL/Auth/Message.thy
--- 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}"