1.1 --- a/src/HOL/IMPP/Natural.thy	Thu Feb 28 12:43:28 2013 +0100
     1.2 +++ b/src/HOL/IMPP/Natural.thy	Thu Feb 28 13:19:25 2013 +0100
     1.3 @@ -122,8 +122,7 @@
     1.4  
     1.5  lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"
     1.6  apply (erule evaln.induct)
     1.7 -apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac @{thm Suc_le_D_lemma}, REPEAT o smp_tac 1]) *})
     1.8 -apply (tactic {* ALLGOALS (resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
     1.9 +apply (auto elim!: Suc_le_D_lemma)
    1.10  done
    1.11  
    1.12  lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"