changeset 2269 | 820f68aec6ee |
parent 2264 | f298678bd54a |
child 2284 | 80ebd1a213fd |
--- a/src/HOL/Auth/Yahalom.ML Thu Nov 28 12:09:33 1996 +0100 +++ b/src/HOL/Auth/Yahalom.ML Thu Nov 28 12:28:52 1996 +0100 @@ -402,7 +402,8 @@ by (REPEAT_FIRST (fast_tac (!claset addSEs partsEs addSDs [Says_imp_sees_Spy RS parts.Inj] - addDs [impOfSubs analz_subset_parts, + addEs [leD RS notE] + addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un, Suc_leD] addss (!simpset))));