src/HOL/Inductive.thy
changeset 33959 2afc55e8ed27
parent 32701 5059a733a4b8
child 33963 977b94b64905
     1.1 --- a/src/HOL/Inductive.thy	Wed Nov 25 09:14:28 2009 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Nov 25 11:16:57 2009 +0100
     1.3 @@ -5,16 +5,15 @@
     1.4  header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
     1.5  
     1.6  theory Inductive 
     1.7 -imports Lattices Sum_Type
     1.8 +imports Complete_Lattice
     1.9  uses
    1.10    ("Tools/inductive.ML")
    1.11    "Tools/dseq.ML"
    1.12    ("Tools/inductive_codegen.ML")
    1.13 -  ("Tools/Datatype/datatype_aux.ML")
    1.14 -  ("Tools/Datatype/datatype_prop.ML")
    1.15 -  ("Tools/Datatype/datatype_rep_proofs.ML")
    1.16 +  "Tools/Datatype/datatype_aux.ML"
    1.17 +  "Tools/Datatype/datatype_prop.ML"
    1.18 +  "Tools/Datatype/datatype_case.ML"
    1.19    ("Tools/Datatype/datatype_abs_proofs.ML")
    1.20 -  ("Tools/Datatype/datatype_case.ML")
    1.21    ("Tools/Datatype/datatype.ML")
    1.22    ("Tools/old_primrec.ML")
    1.23    ("Tools/primrec.ML")
    1.24 @@ -282,11 +281,7 @@
    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_rep_proofs.ML"
    1.31  use "Tools/Datatype/datatype_abs_proofs.ML"
    1.32 -use "Tools/Datatype/datatype_case.ML"
    1.33  use "Tools/Datatype/datatype.ML"
    1.34  setup Datatype.setup
    1.35