src/HOL/Inductive.thy
changeset 45890 5f70aaecae26
parent 44860 56101fa00193
child 45891 d73605c829cc
     1.1 --- a/src/HOL/Inductive.thy	Thu Dec 15 14:11:57 2011 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Thu Dec 15 17:37:14 2011 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4    "Tools/Datatype/datatype_case.ML"
     1.5    ("Tools/Datatype/datatype_abs_proofs.ML")
     1.6    ("Tools/Datatype/datatype_data.ML")
     1.7 +  ("Tools/Datatype/rep_datatype.ML")
     1.8    ("Tools/primrec.ML")
     1.9    ("Tools/Datatype/datatype_codegen.ML")
    1.10  begin
    1.11 @@ -279,6 +280,8 @@
    1.12  use "Tools/Datatype/datatype_data.ML"
    1.13  setup Datatype_Data.setup
    1.14  
    1.15 +use "Tools/Datatype/rep_datatype.ML"
    1.16 +
    1.17  use "Tools/Datatype/datatype_codegen.ML"
    1.18  setup Datatype_Codegen.setup
    1.19