--- a/src/HOL/Transitive_Closure.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Transitive_Closure.thy Sun Nov 15 12:39:51 2015 +0100
@@ -20,6 +20,10 @@
operands to be atomic.
\<close>
+context
+ notes [[inductive_defs]]
+begin
+
inductive_set
rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_^*)" [1000] 999)
for r :: "('a \<times> 'a) set"
@@ -39,6 +43,8 @@
trancl_def [nitpick_unfold del]
tranclp_def [nitpick_unfold del]
+end
+
notation
rtranclp ("(_^**)" [1000] 1000) and
tranclp ("(_^++)" [1000] 1000)