diff -r d9527f97246e -r 89669c58e506 Prod.ML
--- a/Prod.ML	Thu Aug 25 10:47:33 1994 +0200
+++ b/Prod.ML	Thu Aug 25 11:01:45 1994 +0200
@@ -102,6 +102,10 @@
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
 val splitE = result();
 
+goal Prod.thy "!!R a b. split(R,<a,b>) ==> R(a,b)";
+by (etac (split RS iffD1) 1);
+val splitD = result();
+
 goal Prod.thy "!!a b c. z: c(a,b) ==> z: split(c, <a,b>)";
 by (asm_simp_tac pair_ss 1);
 val mem_splitI = result();