src/HOL/Product_Type.thy
changeset 36664 6302f9ad7047
parent 36622 e393a91f86df
child 37136 e0c9d3e49e15
     1.1 --- a/src/HOL/Product_Type.thy	Tue May 04 13:11:15 2010 -0700
     1.2 +++ b/src/HOL/Product_Type.thy	Wed May 05 00:59:59 2010 +0200
     1.3 @@ -416,7 +416,7 @@
     1.4    by (simp add: split_def id_def)
     1.5  
     1.6  lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
     1.7 -  -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity Datatype. *}
     1.8 +  -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
     1.9    by (rule ext) auto
    1.10  
    1.11  lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
    1.12 @@ -752,7 +752,7 @@
    1.13  
    1.14  text {*
    1.15    @{term prod_fun} --- action of the product functor upon
    1.16 -  Datatypes.
    1.17 +  functions.
    1.18  *}
    1.19  
    1.20  definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where