diff -r a4896058a47e -r d0266c81a85e src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Jan 26 13:43:36 1996 +0100
+++ b/src/HOL/Prod.ML	Fri Jan 26 20:25:39 1996 +0100
@@ -122,6 +122,11 @@
 (*These rules are for use with fast_tac.
   Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
 
+goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
+by(split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "splitI2";
+
 goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
 by (Asm_simp_tac 1);
 qed "splitI";
@@ -139,6 +144,11 @@
 by (Asm_simp_tac 1);
 qed "mem_splitI";
 
+goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
+by(split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "mem_splitI2";
+
 val prems = goalw Prod.thy [split_def]
     "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
@@ -258,8 +268,8 @@
 by (rtac (Rep_Unit_inverse RS sym) 1);
 qed "unit_eq";
 
-val prod_cs = set_cs addSIs [SigmaI, mem_splitI] 
+val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2] 
                      addIs  [fst_imageI, snd_imageI, prod_fun_imageI]
-                     addSEs [SigmaE2, SigmaE, mem_splitE, 
+                     addSEs [SigmaE2, SigmaE, splitE, mem_splitE, 
 			     fst_imageE, snd_imageE, prod_fun_imageE,
 			     Pair_inject];