# HG changeset patch
# User oheimb
# Date 991320615 -7200
# Node ID 3fb4d00b294acccc7e6debad51fca0807e9baafb
# Parent  779d289255f7ee98290e91e1d8698fce54e65feb
added injective_fst_snd

diff -r 779d289255f7 -r 3fb4d00b294a src/HOL/Product_Type_lemmas.ML
--- a/src/HOL/Product_Type_lemmas.ML	Thu May 31 16:50:14 2001 +0200
+++ b/src/HOL/Product_Type_lemmas.ML	Thu May 31 16:50:15 2001 +0200
@@ -128,7 +128,6 @@
 qed "surj_pair";
 Addsimps [surj_pair];
 
-
 bind_thm ("split_paired_all",
   SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
 bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]);
@@ -140,7 +139,6 @@
 which cannot be solved by reflexivity.
 *)
 
-
 (* replace parameters of product type by individual component parameters *)
 val safe_full_simp_tac = generic_simp_tac true (true, false, false);
 local (* filtering with exists_paired_all is an essential optimization *)
@@ -404,6 +402,10 @@
 qed "Eps_split_eq";
 *)
 
+Goal "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y";
+by Auto_tac;
+qed "injective_fst_snd";
+
 (*** prod_fun -- action of the product functor upon functions ***)
 
 Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";