src/HOL/Datatype.thy
changeset 33968 f94fb13ecbb3
parent 33963 977b94b64905
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/Datatype.thy	Mon Nov 30 11:42:48 2009 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Mon Nov 30 11:42:49 2009 +0100
     1.3 @@ -1,16 +1,13 @@
     1.4  (*  Title:      HOL/Datatype.thy
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     1.7 -
     1.8 -Could <*> be generalized to a general summation (Sigma)?
     1.9  *)
    1.10  
    1.11 -header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
    1.12 +header {* Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
    1.13  
    1.14  theory Datatype
    1.15  imports Product_Type Sum_Type Nat
    1.16  uses
    1.17 -  ("Tools/Datatype/datatype_rep_proofs.ML")
    1.18    ("Tools/Datatype/datatype.ML")
    1.19    ("Tools/inductive_realizer.ML")
    1.20    ("Tools/Datatype/datatype_realizer.ML")
    1.21 @@ -520,13 +517,12 @@
    1.22  hide (open) type node item
    1.23  hide (open) const Push Node Atom Leaf Numb Lim Split Case
    1.24  
    1.25 -use "Tools/Datatype/datatype_rep_proofs.ML"
    1.26  use "Tools/Datatype/datatype.ML"
    1.27  
    1.28  use "Tools/inductive_realizer.ML"
    1.29  setup InductiveRealizer.setup
    1.30  
    1.31  use "Tools/Datatype/datatype_realizer.ML"
    1.32 -setup DatatypeRealizer.setup
    1.33 +setup Datatype_Realizer.setup
    1.34  
    1.35  end