# HG changeset patch
# User paulson
# Date 985253326 -3600
# Node ID 4b71d38fa6e6da34a94a437bff879c638b588893
# Parent  54a86efcb0ba6ee86805ee68d6cf6d953a60f729
new theorem analz_isSymKey_Decrypt

diff -r 54a86efcb0ba -r 4b71d38fa6e6 src/HOL/Auth/Public_lemmas.ML
--- 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 **)