src/HOL/Product_Type.thy

   (Haskell infix 4 "==")
 
 
 subsubsection {* Fundamental operations and properties *}
 
+lemma Pair_inject:
+  assumes "(a, b) = (a', b')"
+    and "a = a' ==> b = b' ==> R"
+  shows R
+  using assms by simp
+
 lemma surj_pair [simp]: "EX x y. p = (x, y)"
   by (cases p) simp
 
 definition fst :: "'a \<times> 'b \<Rightarrow> 'a" where
   "fst p = (case p of (a, b) \<Rightarrow> a)"

 
 lemma PairE:
   obtains x y where "p = (x, y)"
   by (fact prod.exhaust)
 
-lemma Pair_inject:
-  assumes "(a, b) = (a', b')"
-    and "a = a' ==> b = b' ==> R"
-  shows R
-  using assms by simp
-
 lemmas Pair_eq = prod.inject
 
 lemmas split = split_conv  -- {* for backwards compatibility *}
 
 lemmas Pair_fst_snd_eq = prod_eq_iff