# HG changeset patch
# User nipkow
# Date 865618206 -7200
# Node ID 160f18a686b5befd8001b701d3998f6c775cde1e
# Parent  34655a5d2f56758c41bca1c9d5694a16619e1d6a
Added
AddIffs [Pair_eq];
which made
AddSEs [Pair_inject];
redundant.

diff -r 34655a5d2f56 -r 160f18a686b5 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Jun 06 16:02:13 1997 +0200
+++ b/src/HOL/Prod.ML	Fri Jun 06 19:30:06 1997 +0200
@@ -30,11 +30,10 @@
 by (REPEAT (ares_tac (prems@[ProdI]) 1));
 qed "Pair_inject";
 
-AddSEs [Pair_inject];
-
 goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
-by (Blast_tac 1);
+by (blast_tac (!claset addSEs [Pair_inject]) 1);
 qed "Pair_eq";
+AddIffs [Pair_eq];
 
 goalw Prod.thy [fst_def] "fst((a,b)) = a";
 by (blast_tac (!claset addIs [select_equality]) 1);
@@ -88,7 +87,7 @@
 by (rtac refl 1);
 qed "split";
 
-Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq];
+Addsimps [fst_conv, snd_conv, split_paired_All, split];
 
 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
 by (res_inst_tac[("p","s")] PairE 1);