src/HOL/Inductive.thy
changeset 19599 a5c7eb37d14f
parent 18456 8cc35e95450a
child 20604 9dba9c7872c9
     1.1 --- a/src/HOL/Inductive.thy	Tue May 09 10:09:17 2006 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue May 09 10:09:37 2006 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    ("Tools/datatype_rep_proofs.ML")
     1.5    ("Tools/datatype_abs_proofs.ML")
     1.6    ("Tools/datatype_realizer.ML")
     1.7 +  ("Tools/datatype_hooks.ML")
     1.8    ("Tools/datatype_package.ML")
     1.9    ("Tools/datatype_codegen.ML")
    1.10    ("Tools/recfun_codegen.ML")
    1.11 @@ -82,6 +83,10 @@
    1.12  use "Tools/datatype_rep_proofs.ML"
    1.13  use "Tools/datatype_abs_proofs.ML"
    1.14  use "Tools/datatype_realizer.ML"
    1.15 +
    1.16 +use "Tools/datatype_hooks.ML"
    1.17 +setup DatatypeHooks.setup
    1.18 +
    1.19  use "Tools/datatype_package.ML"
    1.20  setup DatatypePackage.setup
    1.21