src/HOL/Auth/OtwayRees_AN.ML
changeset 3730 6933d20f335f
parent 3683 aafe719dff14
child 3919 c036caebfc75
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Sep 29 11:46:33 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Sep 29 11:47:01 1997 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
     1.5  by (etac otway.induct 1);
     1.6  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
     1.7 -by (Step_tac 1);
     1.8 +by (ALLGOALS Clarify_tac);
     1.9  (*Remaining cases: OR3 and OR4*)
    1.10  by (ex_strip_tac 2);
    1.11  by (Blast_tac 2);