src/HOL/Auth/OtwayRees.ML
changeset 2375 14539397fc04
parent 2328 e984c12ce5b4
child 2417 95f275c8476e
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Dec 13 10:18:48 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Dec 13 10:20:55 1996 +0100
     1.3 @@ -165,8 +165,8 @@
     1.4  by (parts_induct_tac 1);
     1.5  by (REPEAT_FIRST (fast_tac (!claset 
     1.6                                addSEs partsEs
     1.7 -                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
     1.8 -                              addEs [leD RS notE]
     1.9 +                              addSDs [Says_imp_sees_Spy RS parts.Inj]
    1.10 +                              addEs  [leD RS notE]
    1.11                                addDs  [impOfSubs analz_subset_parts,
    1.12                                        impOfSubs parts_insert_subset_Un,
    1.13                                        Suc_leD]
    1.14 @@ -257,7 +257,7 @@
    1.15  by (etac otway.induct 1);
    1.16  by analz_Fake_tac;
    1.17  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
    1.18 -by (ALLGOALS (*Takes 14 secs*)
    1.19 +by (ALLGOALS (*Takes 12 secs*)
    1.20      (asm_simp_tac 
    1.21       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
    1.22                           @ pushes)
    1.23 @@ -451,15 +451,14 @@
    1.24  by (etac otway.induct 1);
    1.25  by analz_Fake_tac;
    1.26  by (ALLGOALS
    1.27 -    (asm_full_simp_tac 
    1.28 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
    1.29 -                          analz_insert_Key_newK] @ pushes)
    1.30 -               setloop split_tac [expand_if])));
    1.31 +    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
    1.32 +				       analz_insert_Key_newK] @ pushes)
    1.33 +		            setloop split_tac [expand_if])));
    1.34  (*OR3*)
    1.35  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    1.36                        addss (!simpset addsimps [parts_insert2])) 3);
    1.37  (*OR4, OR2, Fake*) 
    1.38 -by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    1.39 +by (REPEAT_FIRST spy_analz_tac);
    1.40  (*Oops*) (** LEVEL 5 **)
    1.41  by (fast_tac (!claset delrules [disjE]
    1.42                        addDs [unique_session_keys] addss (!simpset)) 1);