src/HOL/Inductive.thy
changeset 12437 6d4e02b6dd43
parent 12023 d982f98e0f0d
child 12920 32292d83367b
     1.1 --- a/src/HOL/Inductive.thy	Mon Dec 10 15:16:49 2001 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Mon Dec 10 15:17:49 2001 +0100
     1.3 @@ -9,11 +9,14 @@
     1.4  theory Inductive = Gfp + Sum_Type + Relation
     1.5  files
     1.6    ("Tools/inductive_package.ML")
     1.7 +  ("Tools/inductive_codegen.ML")
     1.8    ("Tools/datatype_aux.ML")
     1.9    ("Tools/datatype_prop.ML")
    1.10    ("Tools/datatype_rep_proofs.ML")
    1.11    ("Tools/datatype_abs_proofs.ML")
    1.12    ("Tools/datatype_package.ML")
    1.13 +  ("Tools/datatype_codegen.ML")
    1.14 +  ("Tools/recfun_codegen.ML")
    1.15    ("Tools/primrec_package.ML"):
    1.16  
    1.17  
    1.18 @@ -69,6 +72,9 @@
    1.19  
    1.20  text {* Package setup. *}
    1.21  
    1.22 +use "Tools/recfun_codegen.ML"
    1.23 +setup RecfunCodegen.setup
    1.24 +
    1.25  use "Tools/datatype_aux.ML"
    1.26  use "Tools/datatype_prop.ML"
    1.27  use "Tools/datatype_rep_proofs.ML"
    1.28 @@ -76,7 +82,12 @@
    1.29  use "Tools/datatype_package.ML"
    1.30  setup DatatypePackage.setup
    1.31  
    1.32 +use "Tools/datatype_codegen.ML"
    1.33 +setup DatatypeCodegen.setup
    1.34 +
    1.35 +use "Tools/inductive_codegen.ML"
    1.36 +setup InductiveCodegen.setup
    1.37 +
    1.38  use "Tools/primrec_package.ML"
    1.39 -setup PrimrecPackage.setup
    1.40  
    1.41  end