# HG changeset patch
# User oheimb
# Date 949064934 -3600
# Node ID b1a458416c929d804d1c0f469e49e819ab4af096
# Parent  33d23d0a300e0d13cd15ed40b0b8eaa2e7735bdd
added splitE', also to claset

diff -r 33d23d0a300e -r b1a458416c92 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Jan 28 14:07:53 2000 +0100
+++ b/src/HOL/Prod.ML	Fri Jan 28 14:08:54 2000 +0100
@@ -248,6 +248,11 @@
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
 qed "splitE";
 
+val prems = Goalw [split_def]
+    "[| split c p z;  !!x y. [| p = (x,y);  c x y z |] ==> Q |] ==> Q";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+qed "splitE'";
+
 val major::prems = goal Prod.thy 
     "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
 \    |] ==> R";
@@ -274,7 +279,7 @@
 qed "mem_splitE";
 
 AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
-AddSEs [splitE, mem_splitE];
+AddSEs [splitE, splitE', mem_splitE];
 
 (* allows simplifications of nested splits in case of independent predicates *)
 Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";