# HG changeset patch
# User paulson
# Date 874411082 -7200
# Node ID 65ec38fbb265c147441ee2b1406791b29e04581c
# Parent  3b06747c3f37891e3299793ee815861fa55cfd48
Deleted the redundant simprule not_parts_not_analz

diff -r 3b06747c3f37 -r 65ec38fbb265 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Tue Sep 16 13:54:41 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Tue Sep 16 13:58:02 1997 +0200
@@ -344,8 +344,7 @@
 by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac (!simpset addcongs [conj_cong] 
-                            addsimps [analz_insert_eq, not_parts_not_analz, 
-				      analz_insert_freshK]
+                            addsimps [analz_insert_eq, analz_insert_freshK]
                             setloop split_tac [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
diff -r 3b06747c3f37 -r 65ec38fbb265 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 16 13:54:41 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 16 13:58:02 1997 +0200
@@ -268,9 +268,8 @@
 by (etac otway.induct 1);
 by analz_sees_tac;
 by (ALLGOALS
-    (asm_simp_tac (!simpset addcongs [conj_cong] 
-                            addsimps [analz_insert_eq, not_parts_not_analz, 
-				      analz_insert_freshK]
+    (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] 
+                            addsimps [analz_insert_eq, analz_insert_freshK]
                             setloop split_tac [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
diff -r 3b06747c3f37 -r 65ec38fbb265 src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 16 13:54:41 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 16 13:58:02 1997 +0200
@@ -231,8 +231,7 @@
 by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac (!simpset addcongs [conj_cong] 
-                            addsimps [analz_insert_eq, not_parts_not_analz, 
-				      analz_insert_freshK]
+                            addsimps [analz_insert_eq, analz_insert_freshK]
                             setloop split_tac [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
diff -r 3b06747c3f37 -r 65ec38fbb265 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Sep 16 13:54:41 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Tue Sep 16 13:58:02 1997 +0200
@@ -228,8 +228,7 @@
 by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac 
-     (!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
-			 analz_insert_freshK]
+     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
                setloop split_tac [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addDs [unique_session_keys]) 3);
@@ -387,7 +386,7 @@
 by (ALLGOALS  (*22 seconds*)
     (asm_simp_tac 
      (analz_image_freshK_ss addsimps
-        ([all_conj_distrib, not_parts_not_analz, analz_image_freshK,
+        ([all_conj_distrib, analz_image_freshK,
 	  KeyWithNonce_Says, fresh_not_KeyWithNonce, 
 	  imp_disj_not1,  (*Moves NBa~=NB to the front*)
 	  Says_Server_KeyWithNonce] 
@@ -507,8 +506,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])));
 (*Prove YM3 by showing that no NB can also be an NA*)
 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
diff -r 3b06747c3f37 -r 65ec38fbb265 src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Tue Sep 16 13:54:41 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Tue Sep 16 13:58:02 1997 +0200
@@ -232,8 +232,7 @@
 by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac 
-     (!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
-			 analz_insert_freshK]
+     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
                setloop split_tac [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addDs [unique_session_keys]) 3);