# HG changeset patch
# User paulson
# Date 905523982 -7200
# Node ID 93c21fee39f81b0f3c8256cbfb172905bb2d8083
# Parent  5a5dfb0f0d7db402f87020737a806dac118f339d
tidied

diff -r 5a5dfb0f0d7d -r 93c21fee39f8 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Fri Sep 11 16:25:40 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Fri Sep 11 16:26:22 1998 +0200
@@ -239,7 +239,7 @@
      (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
 			  pushes @ split_ifs))));
 (*Oops*)
-by (blast_tac (claset() addSDs [unique_session_keys]) 5);
+by (blast_tac (claset() addDs [unique_session_keys]) 5);
 (*NS3, replay sub-case*) 
 by (Blast_tac 4);
 (*NS2*)
@@ -252,8 +252,9 @@
 by (assume_tac 2);
 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
 			       Crypt_Spy_analz_bad]) 1);
+(*PROOF FAILED if addDs*)
 by (blast_tac (claset() addSDs [unique_session_keys]) 1);
-val lemma = result() RS mp RS mp RSN(2,rev_notE);
+qed_spec_mp "lemma2";
 
 
 (*Final version: Server's message in the most abstract form*)
@@ -263,7 +264,8 @@
 \           A ~: bad;  B ~: bad;  evs : ns_shared                \
 \        |] ==> Key K ~: analz (spies evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (blast_tac (claset() addSDs [lemma]) 1);
+by (blast_tac (claset() delrules [notI]
+			addIs [lemma2]) 1);
 qed "Spy_not_see_encrypted_key";