# HG changeset patch
# User paulson
# Date 985253366 -3600
# Node ID c4c210e7c89cc2616556cbf0d7bfc1e772ea8982
# Parent  4b71d38fa6e6da34a94a437bff879c638b588893
new theorem analz_Decrypt'

diff -r 4b71d38fa6e6 -r c4c210e7c89c src/HOL/Auth/Shared_lemmas.ML
--- 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! **)