Deleted the redundant simprule not_parts_not_analz

--- a/src/HOL/Auth/NS_Public.ML	Tue Sep 16 13:58:02 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML	Tue Sep 16 14:04:10 1997 +0200
@@ -124,8 +124,7 @@
 fun analz_induct_tac i = 
     etac ns_public.induct i   THEN
     ALLGOALS (asm_simp_tac 
-              (!simpset addsimps [not_parts_not_analz]
-                        setloop split_tac [expand_if]));
+              (!simpset setloop split_tac [expand_if]));
 
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)

--- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Sep 16 13:58:02 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Tue Sep 16 14:04:10 1997 +0200
@@ -127,8 +127,7 @@
 fun analz_induct_tac i = 
     etac ns_public.induct i   THEN
     ALLGOALS (asm_simp_tac 
-              (!simpset addsimps [not_parts_not_analz]
-                        setloop split_tac [expand_if]));
+              (!simpset setloop split_tac [expand_if]));
 
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)

--- a/src/HOL/Auth/NS_Shared.ML	Tue Sep 16 13:58:02 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Tue Sep 16 14:04:10 1997 +0200
@@ -27,6 +27,14 @@
 by possibility_tac;
 result();
 
+goal thy 
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
+\        ==> EX evs: ns_shared.          \
+\               Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
+          ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
+by possibility_tac;
 
 (**** Inductive proofs about ns_shared ****)
 
@@ -264,8 +272,7 @@
 by analz_sees_tac;
 by (ALLGOALS 
     (asm_simp_tac 
-     (!simpset addsimps ([analz_insert_eq, not_parts_not_analz, 
-			  analz_insert_freshK] @ pushes)
+     (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
                setloop split_tac [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addDs [unique_session_keys]) 5);