--- a/src/HOL/Auth/Message.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Message.ML Tue Dec 16 15:17:26 1997 +0100
@@ -18,11 +18,19 @@
AddIffs atomic.inject;
AddIffs msg.inject;
-(*Holds because Friend is injective: thus cannot prove for all f*)
+(*Equations hold because constructors are injective; cannot prove for all f*)
goal thy "(Friend x : Friend``A) = (x:A)";
by (Auto_tac());
qed "Friend_image_eq";
-Addsimps [Friend_image_eq];
+
+goal thy "(Key x : Key``A) = (x:A)";
+by (Auto_tac());
+qed "Key_image_eq";
+
+goal thy "(Nonce x ~: Key``A)";
+by (Auto_tac());
+qed "Nonce_Key_image_eq";
+Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
(** Inverse of keys **)