# HG changeset patch
# User boehmes
# Date 1270543696 -7200
# Node ID 13f0e77128f8a3e06ef95e61f27cf9e1ef72eb33
# Parent  882403378a4124bae173a686bdc3da9a25930794# Parent  2e0370c03066f7990c97f03c58b6b7767a989a6f
merged

diff -r 882403378a41 -r 13f0e77128f8 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Tue Apr 06 10:46:28 2010 +0200
+++ b/src/HOLCF/Fix.thy	Tue Apr 06 10:48:16 2010 +0200
@@ -34,16 +34,10 @@
   "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.
-  This property is essential since monotonicity of iterate makes no sense.
-*}
-
-lemma chain_iterate2: "x \<sqsubseteq> F\<cdot>x \<Longrightarrow> chain (\<lambda>i. iterate i\<cdot>F\<cdot>x)"
-by (rule chainI, induct_tac i, auto elim: monofun_cfun_arg)
+text {* The sequence of function iterations is a chain. *}
 
 lemma chain_iterate [simp]: "chain (\<lambda>i. iterate i\<cdot>F\<cdot>\<bottom>)"
-by (rule chain_iterate2 [OF minimal])
+by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal)
 
 
 subsection {* Least fixed point operator *}