src/HOL/Auth/OtwayRees.ML
changeset 2264 f298678bd54a
parent 2214 f869dc885841
child 2284 80ebd1a213fd
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed Nov 27 20:36:33 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Nov 28 10:41:14 1996 +0100
     1.3 @@ -136,7 +136,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))));
    1.13 @@ -165,7 +166,8 @@
    1.14  by (REPEAT_FIRST (fast_tac (!claset 
    1.15                                addSEs partsEs
    1.16                                addSDs  [Says_imp_sees_Spy RS parts.Inj]
    1.17 -                              addDs  [impOfSubs analz_subset_parts,
    1.18 +                              addEs [leD RS notE]
    1.19 +			      addDs  [impOfSubs analz_subset_parts,
    1.20                                        impOfSubs parts_insert_subset_Un,
    1.21                                        Suc_leD]
    1.22                                addss (!simpset))));