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