fix looping simp rule
authorhuffman
Wed, 17 Feb 2010 09:22:40 -0800
changeset 35170 bb1d1c6a10bb
parent 35169 31cbcb019003
child 35171 28f824c7addc
child 35174 e15040ae75d7
fix looping simp rule
src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Wed Feb 17 09:08:58 2010 -0800
+++ b/src/HOLCF/ex/Loop.thy	Wed Feb 17 09:22:40 2010 -0800
@@ -115,7 +115,7 @@
   and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
 prefer 2 apply (assumption)
 apply (simp add: step_def2)
-apply (simp del: iterate_Suc add: loop_lemma2)
+apply (drule (1) loop_lemma2, simp)
 done
 
 lemma loop_lemma4 [rule_format]: