# HG changeset patch
# User wenzelm
# Date 1362053965 -3600
# Node ID 4cca272150ab7c40e5e6ed5619518717059787f0
# Parent  de47a499bc0489036458f5cce82f02ce87d75cad
tuned proof;

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]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -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: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"