src/HOL/Product_Type.thy

 lemma pair_collapse [simp]: "(fst p, snd p) = p"
   by (cases p) simp
 
 lemmas surjective_pairing = pair_collapse [symmetric]
 
-lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
+lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
   by (cases s, cases t) simp
 
 lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
-  by (simp add: Pair_fst_snd_eq)
+  by (simp add: prod_eq_iff)
 
 lemma split_conv [simp, code]: "split f (a, b) = f a b"
   by (fact prod.cases)
 
 lemma splitI: "f a b \<Longrightarrow> split f (a, b)"

 
 lemmas Pair_eq = prod.inject
 
 lemmas split = split_conv  -- {* for backwards compatibility *}
 
+lemmas Pair_fst_snd_eq = prod_eq_iff
+
 end