--- 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!*)
--- 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! **)
--- 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);
--- 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*)