src/HOL/Auth/Message.ML

--- a/src/HOL/Auth/Message.ML	Tue Oct 08 10:18:53 1996 +0200
+++ b/src/HOL/Auth/Message.ML	Tue Oct 08 10:19:31 1996 +0200
@@ -68,6 +68,10 @@
           keysFor_insert_Key, keysFor_insert_MPair,
           keysFor_insert_Crypt];
 
+goalw thy [keysFor_def] "!!H. Crypt X K : H ==> invKey K : keysFor H";
+by (Fast_tac 1);
+qed "Crypt_imp_invKey_keysFor";
+
 
 (**** Inductive relation "parts" ****)