src/HOL/Inductive.thy
changeset 11325 a5e0289dd56c
parent 11003 ee0838d89deb
child 11436 3f74b80d979f
     1.1 --- a/src/HOL/Inductive.thy	Tue May 22 09:26:57 2001 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue May 22 15:10:06 2001 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  Setup packages for inductive sets and types etc.
     1.5  *)
     1.6  
     1.7 -theory Inductive = Gfp + Sum_Type + NatDef
     1.8 +theory Inductive = Gfp + Sum_Type + Relation
     1.9  files
    1.10    ("Tools/induct_method.ML")
    1.11    ("Tools/inductive_package.ML")
    1.12 @@ -82,11 +82,4 @@
    1.13    Ball_def Bex_def
    1.14    inductive_rulify2
    1.15  
    1.16 -
    1.17 -(*belongs to theory Transitive_Closure*)
    1.18 -declare rtrancl_induct [induct set: rtrancl]
    1.19 -declare rtranclE [cases set: rtrancl]
    1.20 -declare trancl_induct [induct set: trancl]
    1.21 -declare tranclE [cases set: trancl]
    1.22 -
    1.23  end