src/HOLCF/ex/Loop.thy
changeset 39159 0dec18004e75
parent 35948 5e7909f0346b
child 40028 9ee4e0ab2964
     1.1 --- a/src/HOLCF/ex/Loop.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOLCF/ex/Loop.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -104,12 +104,12 @@
     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 addsimps [@{thm step_def2}]) 1 *})
     1.9  apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.10  apply (rule mp)
    1.11  apply (erule spec)
    1.12 -apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [thm "iterate_Suc"]
    1.13 -  addsimps [thm "loop_lemma2"]) 1 *})
    1.14 +apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [@{thm iterate_Suc}]
    1.15 +  addsimps [@{thm loop_lemma2}]) 1 *})
    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)