src/HOL/Inductive.thy

 setup InductMethod.setup
 setup InductivePackage.setup
 setup DatatypePackage.setup
 setup PrimrecPackage.setup
 
-theorems [mono] =
+theorems basic_monos [mono] =
    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
    Collect_mono in_mono vimage_mono
    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    not_all not_ex
    Ball_def Bex_def
 
+(*belongs to theory Transitive_Closure*)
+declare rtrancl_induct [induct set: rtrancl]
+declare rtranclE [cases set: rtrancl]
+declare trancl_induct [induct set: trancl]
+declare tranclE [cases set: trancl]
+
 end