src/HOLCF/ex/Loop.thy
changeset 40028 9ee4e0ab2964
parent 39159 0dec18004e75
child 40322 707eb30e8a53
     1.1 --- a/src/HOLCF/ex/Loop.thy	Sat Oct 16 16:39:06 2010 -0700
     1.2 +++ b/src/HOLCF/ex/Loop.thy	Sat Oct 16 17:09:57 2010 -0700
     1.3 @@ -104,12 +104,11 @@
     1.4  apply (simp (no_asm) add: step_def2)
     1.5  apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
     1.6  apply (erule notE)
     1.7 -apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [@{thm step_def2}]) 1 *})
     1.8 -apply (tactic "asm_simp_tac HOLCF_ss 1")
     1.9 +apply (simp add: step_def2)
    1.10 +apply (simp (no_asm_simp))
    1.11  apply (rule mp)
    1.12  apply (erule spec)
    1.13 -apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [@{thm iterate_Suc}]
    1.14 -  addsimps [@{thm loop_lemma2}]) 1 *})
    1.15 +apply (simp (no_asm_simp) del: iterate_Suc add: loop_lemma2)
    1.16  apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
    1.17    and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
    1.18  prefer 2 apply (assumption)