new theorem analz_Decrypt'

--- a/src/HOL/Auth/Shared_lemmas.ML	Thu Mar 22 10:28:46 2001 +0100
+++ b/src/HOL/Auth/Shared_lemmas.ML	Thu Mar 22 10:29:26 2001 +0100
@@ -20,6 +20,13 @@
 (* invKey(shrK A) = shrK A *)
 Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
 
+
+Goal "[| Crypt K X \\<in> analz H;  Key K  \\<in> analz H |] ==> X \\<in> analz H";
+by Auto_tac;  
+qed "analz_Decrypt'";
+AddDs [analz_Decrypt'];
+Delrules [analz.Decrypt];
+
 (** Rewrites should not refer to  initState(Friend i) 
     -- not in normal form! **)