src/HOL/Auth/Yahalom.ML
changeset 2264 f298678bd54a
parent 2170 c5e460f1ebb4
child 2269 820f68aec6ee
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Nov 27 20:36:33 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Nov 28 10:41:14 1996 +0100
     1.3 @@ -123,7 +123,8 @@
     1.4  \                length evs <= length evs' --> \
     1.5  \                Key (newK evs') ~: parts (sees lost Spy evs)";
     1.6  by (parts_induct_tac 1);
     1.7 -by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     1.8 +by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
     1.9 +				    addDs [impOfSubs analz_subset_parts,
    1.10                                             impOfSubs parts_insert_subset_Un,
    1.11                                             Suc_leD]
    1.12                                      addss (!simpset))));