# HG changeset patch
# User bulwahn
# Date 1350476037 -7200
# Node ID cc69be3c8f87e092b13da0fd1ef182dd718a2d03
# Parent  a39deedd5c3f5bb05184c161e594fdc3c259e83c
moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)

diff -r a39deedd5c3f -r cc69be3c8f87 src/HOL/Product_Type.thy
--- 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 *}