src/HOL/Inductive.thy
changeset 45897 65cef0298158
parent 45891 d73605c829cc
child 45899 df887263a379
     1.1 --- a/src/HOL/Inductive.thy	Fri Dec 16 10:38:38 2011 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Fri Dec 16 10:52:35 2011 +0100
     1.3 @@ -7,16 +7,16 @@
     1.4  theory Inductive 
     1.5  imports Complete_Lattices
     1.6  uses
     1.7 +  "Tools/dseq.ML"
     1.8    ("Tools/inductive.ML")
     1.9 -  "Tools/dseq.ML"
    1.10 -  "Tools/Datatype/datatype_aux.ML"
    1.11 -  "Tools/Datatype/datatype_prop.ML"
    1.12 +  ("Tools/Datatype/datatype_aux.ML")
    1.13 +  ("Tools/Datatype/datatype_prop.ML")
    1.14    ("Tools/Datatype/datatype_abs_proofs.ML")
    1.15    ("Tools/Datatype/datatype_data.ML")
    1.16    ("Tools/Datatype/datatype_case.ML")
    1.17    ("Tools/Datatype/rep_datatype.ML")
    1.18 -  ("Tools/primrec.ML")
    1.19    ("Tools/Datatype/datatype_codegen.ML")
    1.20 +  ("Tools/Datatype/primrec.ML")
    1.21  begin
    1.22  
    1.23  subsection {* Least and greatest fixed points *}
    1.24 @@ -276,15 +276,14 @@
    1.25  
    1.26  text {* Package setup. *}
    1.27  
    1.28 +use "Tools/Datatype/datatype_aux.ML"
    1.29 +use "Tools/Datatype/datatype_prop.ML"
    1.30  use "Tools/Datatype/datatype_abs_proofs.ML"
    1.31  use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
    1.32  use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
    1.33  use "Tools/Datatype/rep_datatype.ML"
    1.34 -
    1.35 -use "Tools/Datatype/datatype_codegen.ML"
    1.36 -setup Datatype_Codegen.setup
    1.37 -
    1.38 -use "Tools/primrec.ML"
    1.39 +use "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
    1.40 +use "Tools/Datatype/primrec.ML"
    1.41  
    1.42  text{* Lambda-abstractions with pattern matching: *}
    1.43