# HG changeset patch
# User paulson
# Date 844762771 -7200
# Node ID 0d05468dc80c5b9aa8efc9c06096d79ba375c488
# Parent  884c2eb74eb099a41bbc9d63f97aa130242a92ea
New theorem Crypt_imp_invKey_keysFor

diff -r 884c2eb74eb0 -r 0d05468dc80c 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" ****)