# HG changeset patch
# User Andreas Lochbihler
# Date 1447689732 -3600
# Node ID 7ba83fbac0ae3ad58e556c97e7d3cda7affbf72e
# Parent  d04b1b4fb01548d425f1d7a24d871e4275cd0ed9# Parent  e4d7972402ed764147837796559135e9e851e403
merged

diff -r d04b1b4fb015 -r 7ba83fbac0ae src/HOL/Complete_Partial_Order.thy
--- 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)