Extra fix needed in newN case
authorpaulson
Thu Nov 28 12:28:52 1996 +0100 (1996-11-28)
changeset 2269820f68aec6ee
parent 2268 79a2f085a7fd
child 2270 d7513875b2b8
Extra fix needed in newN case
src/HOL/Auth/Yahalom.ML
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Nov 28 12:09:33 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Nov 28 12:28:52 1996 +0100
     1.3 @@ -402,7 +402,8 @@
     1.4  by (REPEAT_FIRST (fast_tac (!claset 
     1.5                                addSEs partsEs
     1.6                                addSDs  [Says_imp_sees_Spy RS parts.Inj]
     1.7 -                              addDs  [impOfSubs analz_subset_parts,
     1.8 +                              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))));