--- a/src/HOL/Product_Type.thy Tue May 04 13:11:15 2010 -0700
+++ b/src/HOL/Product_Type.thy Wed May 05 00:59:59 2010 +0200
@@ -416,7 +416,7 @@
by (simp add: split_def id_def)
lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
- -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity Datatype. *}
+ -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
by (rule ext) auto
lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
@@ -752,7 +752,7 @@
text {*
@{term prod_fun} --- action of the product functor upon
- Datatypes.
+ functions.
*}
definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where