src/HOL/Auth/OtwayRees_AN.ML
changeset 3674 65ec38fbb265
parent 3543 82f33248d89d
child 3683 aafe719dff14
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 16 13:54:41 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 16 13:58:02 1997 +0200
     1.3 @@ -268,9 +268,8 @@
     1.4  by (etac otway.induct 1);
     1.5  by analz_sees_tac;
     1.6  by (ALLGOALS
     1.7 -    (asm_simp_tac (!simpset addcongs [conj_cong] 
     1.8 -                            addsimps [analz_insert_eq, not_parts_not_analz, 
     1.9 -				      analz_insert_freshK]
    1.10 +    (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] 
    1.11 +                            addsimps [analz_insert_eq, analz_insert_freshK]
    1.12                              setloop split_tac [expand_if])));
    1.13  (*Oops*)
    1.14  by (blast_tac (!claset addSDs [unique_session_keys]) 4);