src/HOL/Bali/Evaln.thy
changeset 39159 0dec18004e75
parent 35069 09154b995ed8
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Bali/Evaln.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -449,9 +449,9 @@
     1.4  lemma evaln_nonstrict [rule_format (no_asm), elim]: 
     1.5    "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
     1.6  apply (erule evaln.induct)
     1.7 -apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
     1.8 +apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma},
     1.9    REPEAT o smp_tac 1, 
    1.10 -  resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
    1.11 +  resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
    1.12  (* 3 subgoals *)
    1.13  apply (auto split del: split_if)
    1.14  done