# HG changeset patch
# User paulson
# Date 983535277 -3600
# Node ID 5d539f1682c3ab2ae93845ce883c8c3d50586d45
# Parent  c6e49929e544ebac1c03d31ba537fb216bbf06bb
streamlined a proof

diff -r c6e49929e544 -r 5d539f1682c3 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Wed Feb 28 12:37:48 2001 +0100
+++ b/src/HOL/Auth/NS_Shared.thy	Fri Mar 02 13:14:37 2001 +0100
@@ -269,15 +269,15 @@
 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
 apply spy_analz  (*Fake*) 
 apply blast      (*NS2*)
-(*NS3, Server sub-case*) (**LEVEL 6 **)
-apply clarify
-apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2])
-apply (blast dest: Says_imp_knows_Spy analz.Inj Crypt_Spy_analz_bad)
-apply assumption
-apply (blast dest: unique_session_keys)+ (*also proves Oops*)
+(*NS3, Server sub-case*) (**LEVEL 8 **)
+apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
+	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
+(*NS3, Spy sub-case; also Oops*) 
+apply (blast dest: unique_session_keys)+ 
 done
 
 
+
 (*Final version: Server's message in the most abstract form*)
 lemma Spy_not_see_encrypted_key:
      "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;