changeset 2134 | 04a71407089d |
parent 2104 | f5c9a91e4b50 |
child 2135 | 80477862ab33 |
--- a/src/HOL/Auth/OtwayRees.ML Mon Oct 28 13:02:37 1996 +0100 +++ b/src/HOL/Auth/OtwayRees.ML Mon Oct 28 15:36:18 1996 +0100 @@ -694,7 +694,7 @@ (*spy_analz_tac just does not work here: it is an entirely different proof!*) by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib, - imp_conj_distrib, parts_insert_sees, + imp_conjR, parts_insert_sees, parts_insert2]))); by (REPEAT_FIRST (etac exE)); (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)