# HG changeset patch
# User Andreas Lochbihler
# Date 1447689611 -3600
# Node ID e4d7972402ed764147837796559135e9e851e403
# Parent  95a57e288fd4b6d2315385ee463b4e494ebc5194
export internal definition

diff -r 95a57e288fd4 -r e4d7972402ed src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Mon Nov 16 14:27:10 2015 +0100
+++ b/src/HOL/Complete_Partial_Order.thy	Mon Nov 16 17:00:11 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)