| changeset 17956 | 369e2af8ee45 |
| parent 17477 | ceb42ea2f223 |
| child 18447 | da548623916a |
--- a/src/HOL/IMPP/Hoare.ML Fri Oct 21 18:14:32 2005 +0200 +++ b/src/HOL/IMPP/Hoare.ML Fri Oct 21 18:14:34 2005 +0200 @@ -268,7 +268,7 @@ by (resolve_tac (premises()(*hoare_derivs.asm*)) 1); by (Fast_tac 1); by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1); -byev[dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3]; +by (EVERY [dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3]); by (eresolve_tac (tl(tl(tl(premises())))) 3); by (Fast_tac 1); by (dtac finite_subset 1);