--- a/src/HOL/Auth/OtwayRees_Bad.ML Wed Nov 27 20:36:33 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Nov 28 10:41:14 1996 +0100
@@ -136,7 +136,8 @@
\ length evs <= length evs' --> \
\ Key (newK evs') ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
-by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
+ addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
@@ -165,6 +166,7 @@
by (REPEAT_FIRST
(fast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un, Suc_leD]
addss (!simpset))));