# HG changeset patch
# User paulson
# Date 854012103 -3600
# Node ID 906704a5b3bf7aace03d5f27ae96f0a3bd8a6e8a
# Parent  1e04eb7f7eb1cb68e2e78b8d97213b17a45ec025
Added sees_Spy_partsEs

diff -r 1e04eb7f7eb1 -r 906704a5b3bf src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Thu Jan 23 10:34:18 1997 +0100
+++ b/src/HOL/Auth/Public.ML	Thu Jan 23 10:35:03 1997 +0100
@@ -129,6 +129,10 @@
 by (Auto_tac ());
 qed_spec_mp "Says_imp_sees_Spy";
 
+(*Use with addSEs to derive contradictions from old Says events containing
+  items known to be fresh*)
+val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
+
 goal thy  
  "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;  C : lost |] \
 \        ==> X : analz (sees lost Spy evs)";