--- a/src/HOL/Product_Type.thy Wed Oct 17 14:13:57 2012 +0200
+++ b/src/HOL/Product_Type.thy Wed Oct 17 14:13:57 2012 +0200
@@ -306,6 +306,12 @@
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
@@ -1140,12 +1146,6 @@
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 *}