--- 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