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