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