--- a/src/HOL/Product_Type.thy Thu Nov 12 15:50:05 2009 +0100
+++ b/src/HOL/Product_Type.thy Thu Nov 12 17:21:43 2009 +0100
@@ -777,7 +777,7 @@
"apfst f (x, y) = (f x, y)"
by (simp add: apfst_def)
-lemma upd_snd_conv [simp, code]:
+lemma apsnd_conv [simp, code]:
"apsnd f (x, y) = (x, f y)"
by (simp add: apsnd_def)
@@ -829,6 +829,9 @@
"apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
by (cases x) simp
+lemma apsnd_apfst_commute:
+ "apsnd f (apfst g p) = apfst g (apsnd f p)"
+ by simp
text {*
Disjoint union of a family of sets -- Sigma.