# HG changeset patch
# User paulson
# Date 882873963 -3600
# Node ID 0abf9d3f4391cd11bbf111602596f06941f8f7b1
# Parent  af3239def3d4241a2ca3c1e37f5841e34f1f3feb
Tidied using rev_iffD1

diff -r af3239def3d4 -r 0abf9d3f4391 src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Dec 23 11:43:48 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Dec 23 11:46:03 1997 +0100
@@ -98,12 +98,8 @@
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
+AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
+	Spy_analz_shrK RSN (2, rev_iffD1)];
 
 
 (*Nobody can have used non-existent keys!*)
diff -r af3239def3d4 -r 0abf9d3f4391 src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Tue Dec 23 11:43:48 1997 +0100
+++ b/src/HOL/Auth/Recur.ML	Tue Dec 23 11:46:03 1997 +0100
@@ -164,13 +164,8 @@
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : recur |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-
+AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
+	Spy_analz_shrK RSN (2, rev_iffD1)];
 
 
 (** Nobody can have used non-existent keys! **)
diff -r af3239def3d4 -r 0abf9d3f4391 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Dec 23 11:43:48 1997 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Tue Dec 23 11:46:03 1997 +0100
@@ -92,13 +92,8 @@
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
-\                  evs : yahalom |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
+AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
+	Spy_analz_shrK RSN (2, rev_iffD1)];
 
 
 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
@@ -530,6 +525,7 @@
 by (blast_tac (claset() addDs [Says_unique_NB]) 1 THEN flexflex_tac);
 (*case NB ~= NBa*)
 by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
+by (Clarify_tac 1);
 by (blast_tac (claset() addSEs [MPair_parts]
 		        addDs  [Says_imp_spies RS parts.Inj, 
 			        no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
diff -r af3239def3d4 -r 0abf9d3f4391 src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Tue Dec 23 11:43:48 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Tue Dec 23 11:46:03 1997 +0100
@@ -92,13 +92,8 @@
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
 
-goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
-\                  evs : yahalom |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
+AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
+	Spy_analz_shrK RSN (2, rev_iffD1)];
 
 
 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)