src/HOLCF/Fix.thy

--- a/src/HOLCF/Fix.thy	Wed Jun 18 23:15:41 2008 +0200
+++ b/src/HOLCF/Fix.thy	Thu Jun 19 00:02:08 2008 +0200
@@ -33,7 +33,11 @@
 declare iterate.simps [simp del]
 
 lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)"
-by (induct_tac n, auto)
+by (induct n) simp_all
+
+lemma iterate_iterate:
+  "iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x"
+by (induct m) simp_all
 
 text {*
   The sequence of function iterations is a chain.