src/HOL/Complete_Partial_Order.thy
changeset 62093 bd73a2279fcd
parent 61689 e4d7972402ed
child 63612 7195acc2fe93
     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Thu Jan 07 15:50:09 2016 +0100
     1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Thu Jan 07 15:53:39 2016 +0100
     1.3 @@ -87,7 +87,7 @@
     1.4  
     1.5  subsection \<open>Transfinite iteration of a function\<close>
     1.6  
     1.7 -context notes [[inductive_defs]] begin
     1.8 +context notes [[inductive_internals]] begin
     1.9  
    1.10  inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
    1.11  for f :: "'a \<Rightarrow> 'a"