# HG changeset patch
# User paulson
# Date 866640090 -7200
# Node ID 6d2887123fa03007432138b8e5f1c005671a8c65
# Parent  22db7a9cbb524c6918a3b0419cc5dfd61ce89302
Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost

diff -r 22db7a9cbb52 -r 6d2887123fa0 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Wed Jun 18 15:19:37 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Wed Jun 18 15:21:30 1997 +0200
@@ -296,7 +296,8 @@
 by (step_tac (!claset delrules [impCE]) 1);
 by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
 by (assume_tac 2);
-by (blast_tac (!claset addSDs [Says_Crypt_not_lost]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
+			      Crypt_Spy_analz_lost]) 1);
 by (blast_tac (!claset addDs [unique_session_keys]) 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
@@ -379,7 +380,8 @@
 by (case_tac "Ba : lost" 1);
 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, 
 			      unique_session_keys]) 2);
-by (blast_tac (!claset addDs [Says_Crypt_lost]) 1);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
+			      Crypt_Spy_analz_lost]) 1);
 val lemma = result();
 
 goal thy