author | huffman |
Wed, 17 Feb 2010 09:22:40 -0800 | |
changeset 35170 | bb1d1c6a10bb |
parent 35169 | 31cbcb019003 |
child 35171 | 28f824c7addc |
child 35174 | e15040ae75d7 |
--- 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]: