# HG changeset patch
# User oheimb
# Date 991320686 -7200
# Node ID d5f1b482bfbfdf338e0bea14bc676b821be100af
# Parent  442b9bc808a5468df80e2f4d77673da04f1a03f7
replaced Sel_injective_cprod by new injective_fst_snd

diff -r 442b9bc808a5 -r d5f1b482bfbf src/HOLCF/Cprod1.ML
--- a/src/HOLCF/Cprod1.ML	Thu May 31 16:51:14 2001 +0200
+++ b/src/HOLCF/Cprod1.ML	Thu May 31 16:51:26 2001 +0200
@@ -11,20 +11,12 @@
 (* less_cprod is a partial order on 'a * 'b                                 *)
 (* ------------------------------------------------------------------------ *)
 
-(*###TO Product_Type_lemmas.ML *)
-Goal "[|fst x = fst y; snd x = snd y|] ==> x = y";
-by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
-by (rotate_tac ~1 1);
-by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
-by (asm_simp_tac (simpset_of (theory "Product_Type")) 1);
-qed "Sel_injective_cprod";
-
 Goalw [less_cprod_def] "(p::'a*'b) << p";
 by (Simp_tac 1);
 qed "refl_less_cprod";
 
 Goalw [less_cprod_def] "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2";
-by (rtac Sel_injective_cprod 1);
+by (rtac injective_fst_snd 1);
 by (fast_tac (HOL_cs addIs [antisym_less]) 1);
 by (fast_tac (HOL_cs addIs [antisym_less]) 1);
 qed "antisym_less_cprod";