--- a/src/HOL/Auth/OtwayRees.ML Thu Jun 19 11:28:55 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Thu Jun 19 11:31:14 1997 +0200
@@ -192,10 +192,10 @@
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+(*Fake*)
+by (spy_analz_tac 2);
(*Base*)
by (Blast_tac 1);
-(*Fake, OR2, OR4*)
-by (REPEAT (spy_analz_tac 1));
qed_spec_mp "analz_image_freshK";
@@ -365,16 +365,18 @@
by analz_sees_tac;
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
- addsimps [not_parts_not_analz, analz_insert_freshK]
+ addsimps [analz_insert_eq, not_parts_not_analz,
+ analz_insert_freshK]
setloop split_tac [expand_if])));
+(*Oops*)
+by (blast_tac (!claset addSDs [unique_session_keys]) 4);
+(*OR4*)
+by (Blast_tac 3);
(*OR3*)
-by (blast_tac (!claset delrules [impCE]
- addSEs sees_Spy_partsEs
- addIs [impOfSubs analz_subset_parts]) 3);
-(*OR4, OR2, Fake*)
-by (REPEAT_FIRST spy_analz_tac);
-(*Oops*) (** LEVEL 5 **)
-by (blast_tac (!claset addSDs [unique_session_keys]) 1);
+by (blast_tac (!claset addSEs sees_Spy_partsEs
+ addIs [impOfSubs analz_subset_parts]) 2);
+(*Fake*)
+by (spy_analz_tac 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy