--- a/src/HOL/Complete_Partial_Order.thy Mon Nov 16 15:59:47 2015 +0100
+++ b/src/HOL/Complete_Partial_Order.thy Mon Nov 16 17:02:12 2015 +0100
@@ -87,12 +87,16 @@
subsection \<open>Transfinite iteration of a function\<close>
+context notes [[inductive_defs]] begin
+
inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
for f :: "'a \<Rightarrow> 'a"
where
step: "x \<in> iterates f \<Longrightarrow> f x \<in> iterates f"
| Sup: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> Sup M \<in> iterates f"
+end
+
lemma iterates_le_f:
"x \<in> iterates f \<Longrightarrow> monotone (op \<le>) (op \<le>) f \<Longrightarrow> x \<le> f x"
by (induct x rule: iterates.induct)