src/ZF/Inductive.thy
changeset 16417 9bc16273c2d4
parent 13357 6f54e992777e
child 22814 4cd25f1706bb
     1.1 --- a/src/ZF/Inductive.thy	Fri Jun 17 11:35:35 2005 +0200
     1.2 +++ b/src/ZF/Inductive.thy	Fri Jun 17 16:12:49 2005 +0200
     1.3 @@ -7,14 +7,14 @@
     1.4  
     1.5  header{*Inductive and Coinductive Definitions*}
     1.6  
     1.7 -theory Inductive = Fixedpt + QPair
     1.8 -  files
     1.9 +theory Inductive imports Fixedpt QPair
    1.10 +  uses
    1.11      "ind_syntax.ML"
    1.12      "Tools/cartprod.ML"
    1.13      "Tools/ind_cases.ML"
    1.14      "Tools/inductive_package.ML"
    1.15      "Tools/induct_tacs.ML"
    1.16 -    "Tools/primrec_package.ML":
    1.17 +    "Tools/primrec_package.ML" begin
    1.18  
    1.19  setup IndCases.setup
    1.20  setup DatatypeTactics.setup