src/HOL/Transitive_Closure.thy

--- a/src/HOL/Transitive_Closure.thy	Thu Jan 07 15:50:09 2016 +0100
+++ b/src/HOL/Transitive_Closure.thy	Thu Jan 07 15:53:39 2016 +0100
@@ -21,7 +21,7 @@
 \<close>
 
 context
-  notes [[inductive_defs]]
+  notes [[inductive_internals]]
 begin
 
 inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>*)" [1000] 999)