diff -r 3b53ed2c846f -r 4c5a03649af7 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Oct 23 22:11:43 2000 +0200
+++ b/src/HOL/Inductive.thy	Mon Oct 23 22:12:04 2000 +0200
@@ -18,11 +18,17 @@
 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