src/HOL/Auth/NS_Public.ML

--- a/src/HOL/Auth/NS_Public.ML	Fri Dec 13 10:17:35 1996 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Fri Dec 13 10:18:48 1996 +0100
@@ -114,7 +114,7 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS
     (asm_simp_tac 
-     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+     (!simpset addsimps ([not_parts_not_analz] @ pushes)
                setloop split_tac [expand_if])));
 (*NS3*)
 by (fast_tac (!claset addSEs partsEs
@@ -123,13 +123,12 @@
 by (fast_tac (!claset addSEs partsEs
                       addEs  [nonce_not_seen_now]) 3);
 (*Fake*)
-by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
+by (best_tac (!claset addIs [analz_insertI]
 		      addDs [impOfSubs analz_subset_parts,
 			     impOfSubs Fake_parts_insert]
 	              addss (!simpset)) 2);
 (*Base*)
-by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
-                      addss (!simpset)) 1);
+by (fast_tac (!claset addss (!simpset)) 1);
 bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
 
 
@@ -143,7 +142,7 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS 
     (asm_simp_tac 
-     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+     (!simpset addsimps ([not_parts_not_analz] @ pushes)
                setloop split_tac [expand_if])));
 (*NS1*)
 by (expand_case_tac "NA = ?y" 3 THEN
@@ -152,7 +151,7 @@
 by (fast_tac (!claset addss (!simpset)) 1);
 (*Fake*)
 by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
+by (step_tac (!claset addSIs [analz_insertI]) 1);
 by (ex_strip_tac 1);
 by (best_tac (!claset delrules [conjI]
 		      addSDs [impOfSubs Fake_parts_insert]
@@ -183,7 +182,7 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS 
     (asm_simp_tac 
-     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+     (!simpset addsimps ([not_parts_not_analz] @ pushes)
                setloop split_tac [expand_if])));
 (*NS3*)
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
@@ -193,7 +192,7 @@
                       addSDs [new_nonces_not_seen, 
 			      Says_imp_sees_Spy' RS parts.Inj]) 2);
 (*Fake*)
-by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
 (*NS2*)
 by (Step_tac 1);
 by (fast_tac (!claset addSEs partsEs
@@ -252,12 +251,12 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS
     (asm_simp_tac 
-     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+     (!simpset addsimps ([not_parts_not_analz] @ pushes)
                setloop split_tac [expand_if])));
 (*Fake*)
 by (best_tac (!claset addSIs [disjI2]
 		      addSDs [impOfSubs Fake_parts_insert]
-		      addIs  [impOfSubs (subset_insertI RS analz_mono)]
+		      addIs  [analz_insertI]
 		      addDs  [impOfSubs analz_subset_parts]
 	              addss (!simpset)) 2);
 (*Base*)
@@ -280,7 +279,7 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS 
     (asm_simp_tac 
-     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+     (!simpset addsimps ([not_parts_not_analz] @ pushes)
                setloop split_tac [expand_if])));
 (*NS2*)
 by (expand_case_tac "NB = ?y" 3 THEN
@@ -289,7 +288,7 @@
 by (fast_tac (!claset addss (!simpset)) 1);
 (*Fake*)
 by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
-by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
+by (step_tac (!claset addSIs [analz_insertI]) 1);
 by (ex_strip_tac 1);
 by (best_tac (!claset delrules [conjI]
 	              addSDs [impOfSubs Fake_parts_insert]
@@ -323,7 +322,7 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS 
     (asm_simp_tac 
-     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
+     (!simpset addsimps ([not_parts_not_analz] @ pushes)
                setloop split_tac [expand_if])));
 (*NS3*)
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
@@ -333,7 +332,7 @@
                       addSDs [new_nonces_not_seen, 
 			      Says_imp_sees_Spy' RS parts.Inj]) 2);
 (*Fake*)
-by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
 (*NS2*)
 by (Step_tac 1);
 by (fast_tac (!claset addSEs partsEs