--- a/src/HOL/Auth/OtwayRees.ML Fri Dec 13 10:18:48 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Fri Dec 13 10:20:55 1996 +0100
@@ -165,8 +165,8 @@
by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addEs [leD RS notE]
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
@@ -257,7 +257,7 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 14 secs*)
+by (ALLGOALS (*Takes 12 secs*)
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@ pushes)
@@ -451,15 +451,14 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_full_simp_tac
- (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
- analz_insert_Key_newK] @ pushes)
- setloop split_tac [expand_if])));
+ (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
+ analz_insert_Key_newK] @ pushes)
+ setloop split_tac [expand_if])));
(*OR3*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset addsimps [parts_insert2])) 3);
(*OR4, OR2, Fake*)
-by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
+by (REPEAT_FIRST spy_analz_tac);
(*Oops*) (** LEVEL 5 **)
by (fast_tac (!claset delrules [disjE]
addDs [unique_session_keys] addss (!simpset)) 1);