changeset 5535 | 678999604ee9 |
parent 5492 | d9fc3457554e |
child 6308 | 76f3865a2b1d |
--- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Sep 22 17:08:30 1998 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Wed Sep 23 10:03:32 1998 +0200 @@ -199,7 +199,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addcongs [conj_cong] addsimps [analz_insert_eq, analz_insert_freshK] - addsimps (pushes@split_ifs)))); + @ pushes @ split_ifs))); (*Oops*) by (blast_tac (claset() addSDs [unique_session_keys]) 4); (*OR4*)