diff -r 414e04d7c2d6 -r 8df171ccdbd8 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Wed Sep 17 16:37:27 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Wed Sep 17 16:37:40 1997 +0200
@@ -276,14 +276,14 @@
                setloop split_tac [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addDs [unique_session_keys]) 5);
-(*NS4*) 
+(*NS3, replay sub-case*) 
 by (Blast_tac 4);
 (*NS2*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs
                        addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
 (*Fake*) 
 by (spy_analz_tac 1);
-(*NS3*) (**LEVEL 6 **)
+(*NS3, Server sub-case*) (**LEVEL 6 **)
 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);