src/HOL/Product_Type.thy
changeset 31775 2b04504fcb69
parent 31723 f5cafe803b55
child 32010 cb1a1c94b4cd
     1.1 --- a/src/HOL/Product_Type.thy	Tue Jun 23 12:09:14 2009 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Jun 23 12:09:30 2009 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    ("Tools/split_rule.ML")
     1.5    ("Tools/inductive_set.ML")
     1.6    ("Tools/inductive_realizer.ML")
     1.7 -  ("Tools/datatype_package/datatype_realizer.ML")
     1.8 +  ("Tools/Datatype/datatype_realizer.ML")
     1.9  begin
    1.10  
    1.11  subsection {* @{typ bool} is a datatype *}
    1.12 @@ -399,7 +399,7 @@
    1.13    by (simp add: split_def id_def)
    1.14  
    1.15  lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
    1.16 -  -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
    1.17 +  -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity Datatype. *}
    1.18    by (rule ext) auto
    1.19  
    1.20  lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
    1.21 @@ -734,7 +734,7 @@
    1.22  
    1.23  text {*
    1.24    @{term prod_fun} --- action of the product functor upon
    1.25 -  functions.
    1.26 +  Datatypes.
    1.27  *}
    1.28  
    1.29  definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
    1.30 @@ -1154,7 +1154,7 @@
    1.31  use "Tools/inductive_set.ML"
    1.32  setup Inductive_Set.setup
    1.33  
    1.34 -use "Tools/datatype_package/datatype_realizer.ML"
    1.35 +use "Tools/Datatype/datatype_realizer.ML"
    1.36  setup DatatypeRealizer.setup
    1.37  
    1.38  end