--- a/src/HOL/Inductive.thy Tue May 22 09:26:57 2001 +0200
+++ b/src/HOL/Inductive.thy Tue May 22 15:10:06 2001 +0200
@@ -6,7 +6,7 @@
Setup packages for inductive sets and types etc.
*)
-theory Inductive = Gfp + Sum_Type + NatDef
+theory Inductive = Gfp + Sum_Type + Relation
files
("Tools/induct_method.ML")
("Tools/inductive_package.ML")
@@ -82,11 +82,4 @@
Ball_def Bex_def
inductive_rulify2
-
-(*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