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