src/HOL/Inductive.thy
changeset 31604 eb2f9d709296
parent 29281 b22ccb3998db
child 31723 f5cafe803b55
     1.1 --- a/src/HOL/Inductive.thy	Wed Jun 10 15:04:32 2009 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Wed Jun 10 15:04:33 2009 +0200
     1.3 @@ -10,15 +10,15 @@
     1.4    ("Tools/inductive_package.ML")
     1.5    "Tools/dseq.ML"
     1.6    ("Tools/inductive_codegen.ML")
     1.7 -  ("Tools/datatype_aux.ML")
     1.8 -  ("Tools/datatype_prop.ML")
     1.9 -  ("Tools/datatype_rep_proofs.ML")
    1.10 -  ("Tools/datatype_abs_proofs.ML")
    1.11 -  ("Tools/datatype_case.ML")
    1.12 -  ("Tools/datatype_package.ML")
    1.13 +  ("Tools/datatype_package/datatype_aux.ML")
    1.14 +  ("Tools/datatype_package/datatype_prop.ML")
    1.15 +  ("Tools/datatype_package/datatype_rep_proofs.ML")
    1.16 +  ("Tools/datatype_package/datatype_abs_proofs.ML")
    1.17 +  ("Tools/datatype_package/datatype_case.ML")
    1.18 +  ("Tools/datatype_package/datatype_package.ML")
    1.19    ("Tools/old_primrec_package.ML")
    1.20    ("Tools/primrec_package.ML")
    1.21 -  ("Tools/datatype_codegen.ML")
    1.22 +  ("Tools/datatype_package/datatype_codegen.ML")
    1.23  begin
    1.24  
    1.25  subsection {* Least and greatest fixed points *}
    1.26 @@ -335,17 +335,18 @@
    1.27  
    1.28  text {* Package setup. *}
    1.29  
    1.30 -use "Tools/datatype_aux.ML"
    1.31 -use "Tools/datatype_prop.ML"
    1.32 -use "Tools/datatype_rep_proofs.ML"
    1.33 -use "Tools/datatype_abs_proofs.ML"
    1.34 -use "Tools/datatype_case.ML"
    1.35 -use "Tools/datatype_package.ML"
    1.36 +use "Tools/datatype_package/datatype_aux.ML"
    1.37 +use "Tools/datatype_package/datatype_prop.ML"
    1.38 +use "Tools/datatype_package/datatype_rep_proofs.ML"
    1.39 +use "Tools/datatype_package/datatype_abs_proofs.ML"
    1.40 +use "Tools/datatype_package/datatype_case.ML"
    1.41 +use "Tools/datatype_package/datatype_package.ML"
    1.42  setup DatatypePackage.setup
    1.43 +
    1.44  use "Tools/old_primrec_package.ML"
    1.45  use "Tools/primrec_package.ML"
    1.46  
    1.47 -use "Tools/datatype_codegen.ML"
    1.48 +use "Tools/datatype_package/datatype_codegen.ML"
    1.49  setup DatatypeCodegen.setup
    1.50  
    1.51  use "Tools/inductive_codegen.ML"