Inductive definitions are now introduced earlier in the theory hierarchy.

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

--- a/src/HOL/Nat.thy	Tue May 22 09:26:57 2001 +0200
+++ b/src/HOL/Nat.thy	Tue May 22 15:10:06 2001 +0200
@@ -6,7 +6,7 @@
 and * (for div, mod and dvd, see theory Divides).
 *)
 
-Nat = NatDef + Inductive +
+Nat = NatDef +
 
 (* type "nat" is a wellfounded linear order, and a datatype *)