--- 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))";