src/HOL/Inductive.thy
changeset 25557 ea6b11021e79
parent 25534 d0b74fdd6067
child 26013 8764a1f1253b
     1.1 --- a/src/HOL/Inductive.thy	Thu Dec 06 12:58:01 2007 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Thu Dec 06 15:10:09 2007 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4    ("Tools/datatype_abs_proofs.ML")
     1.5    ("Tools/datatype_case.ML")
     1.6    ("Tools/datatype_package.ML")
     1.7 +  ("Tools/old_primrec_package.ML")
     1.8    ("Tools/primrec_package.ML")
     1.9    ("Tools/datatype_codegen.ML")
    1.10  begin
    1.11 @@ -328,6 +329,7 @@
    1.12  use "Tools/datatype_case.ML"
    1.13  use "Tools/datatype_package.ML"
    1.14  setup DatatypePackage.setup
    1.15 +use "Tools/old_primrec_package.ML"
    1.16  use "Tools/primrec_package.ML"
    1.17  
    1.18  use "Tools/datatype_codegen.ML"