# HG changeset patch
# User nipkow
# Date 757948957 -3600
# Node ID 04f43a28c97a967dffc5912144b03001ea2cfc5f
# Parent  2fdeeae553acf1fa202d871d21a079cfbe4572ea
added pair_eq

diff -r 2fdeeae553ac -r 04f43a28c97a Prod.ML
--- a/Prod.ML	Wed Jan 05 19:39:05 1994 +0100
+++ b/Prod.ML	Fri Jan 07 14:22:37 1994 +0100
@@ -60,6 +60,12 @@
 
 val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
 
+goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
+by(res_inst_tac[("p","s")]PairE 1);
+by(res_inst_tac[("p","t")]PairE 1);
+by(asm_simp_tac pair_ss 1);
+val pair_eq = result();
+
 (*Prevents simplification of c: much faster*)
 val split_weak_cong = prove_goal Prod.thy
   "p=q ==> split(p,c) = split(q,c)"
diff -r 2fdeeae553ac -r 04f43a28c97a prod.ML
--- a/prod.ML	Wed Jan 05 19:39:05 1994 +0100
+++ b/prod.ML	Fri Jan 07 14:22:37 1994 +0100
@@ -60,6 +60,12 @@
 
 val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
 
+goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
+by(res_inst_tac[("p","s")]PairE 1);
+by(res_inst_tac[("p","t")]PairE 1);
+by(asm_simp_tac pair_ss 1);
+val pair_eq = result();
+
 (*Prevents simplification of c: much faster*)
 val split_weak_cong = prove_goal Prod.thy
   "p=q ==> split(p,c) = split(q,c)"