new theorem analz_isSymKey_Decrypt

--- a/src/HOL/Auth/Public_lemmas.ML	Thu Mar 22 10:27:00 2001 +0100
+++ b/src/HOL/Auth/Public_lemmas.ML	Thu Mar 22 10:28:46 2001 +0100
@@ -34,6 +34,11 @@
 
 AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
 
+Goal "[| Crypt K X \\<in> analz H;  isSymKey K;  Key K  \\<in> analz H |] \
+\     ==> X \\<in> analz H";
+by (auto_tac(claset(), simpset() addsimps [isSymKey_def]));
+qed "analz_isSymKey_Decrypt";
+
 
 (** "Image" equations that hold for injective functions **)