# HG changeset patch
# User hoelzl
# Date 1258042903 -3600
# Node ID 548a34929e98d9f5b24ac9792cbaf6f0a7e5100c
# Parent  19a4fe8ecf2420379b71d4f900b11ca739634998
Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute

diff -r 19a4fe8ecf24 -r 548a34929e98 src/HOL/Product_Type.thy
--- 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.