# HG changeset patch
# User berghofe
# Date 990537006 -7200
# Node ID a5e0289dd56c0907ee52e1bd169905fdeeb524b3
# Parent  82406bd816a53d5867bbcafc23e6638f8d1c7dbc
Inductive definitions are now introduced earlier in the theory hierarchy.

diff -r 82406bd816a5 -r a5e0289dd56c src/HOL/Inductive.thy
--- 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
diff -r 82406bd816a5 -r a5e0289dd56c src/HOL/Nat.thy
--- 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 *)