# HG changeset patch
# User paulson
# Date 898247660 -7200
# Node ID 77cc7e7b50f2b1734dc6a67c5513dd4c37d95305
# Parent  75d20f367e94fdd3ff300663d9cedcb2ab4b28ce
tidying

diff -r 75d20f367e94 -r 77cc7e7b50f2 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Fri Jun 19 10:34:33 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Fri Jun 19 11:14:20 1998 +0200
@@ -99,7 +99,7 @@
 (*Fake*)
 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
 (*NS2, NS4, NS5*)
-by (ALLGOALS (Blast_tac));
+by (ALLGOALS Blast_tac);
 qed_spec_mp "new_keys_not_used";
 
 bind_thm ("new_keys_not_analzd",
@@ -386,12 +386,12 @@
 goal thy
  "!!evs. [| B ~: bad;  evs : ns_shared |]                              \
 \        ==> Key K ~: analz (spies evs) -->                            \
-\            Says Server A                                     \
+\            Says Server A                                             \
 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
-\             : set evs -->         \
-\            Says B A (Crypt K (Nonce NB))  : set evs -->  \
-\            Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs) --> \
+\             : set evs -->                                            \
+\            Says B A (Crypt K (Nonce NB))  : set evs -->              \
+\            Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs) -->    \
 \            Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
 by (parts_induct_tac 1);
 (*NS4*)
@@ -407,7 +407,7 @@
 by (Clarify_tac 1);
 by (not_bad_tac "Aa" 1);
 by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1);
-val lemma = result();
+qed_spec_mp "B_trusts_NS5_lemma";
 
 
 (*Very strong Oops condition reveals protocol's weakness*)
@@ -420,6 +420,6 @@
 \        ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
 by (dtac B_trusts_NS3 1);
 by (ALLGOALS Clarify_tac);
-by (blast_tac (claset() addSIs [normalize_thm [RSspec, RSmp] lemma]
+by (blast_tac (claset() addSIs [B_trusts_NS5_lemma]
 	         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
 qed "B_trusts_NS5";