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