src/ZF/pair.ML

--- a/src/ZF/pair.ML	Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/pair.ML	Tue Jun 21 17:20:34 1994 +0200
@@ -103,7 +103,7 @@
 val split = prove_goalw ZF.thy [split_def]
     "split(%x y.c(x,y), <a,b>) = c(a,b)"
  (fn _ =>
-  [ (fast_tac (upair_cs addIs [the_equality] addEs [Pair_inject]) 1) ]);
+  [ (fast_tac (upair_cs addIs [the_equality] addSEs [Pair_inject]) 1) ]);
 
 val split_type = prove_goal ZF.thy
     "[|  p:Sigma(A,B);   \
@@ -114,6 +114,16 @@
     (etac ssubst 1),
     (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
 
+
+goal ZF.thy
+  "!!u. u: A*B ==>   \
+\       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
+by (etac SigmaE 1);
+by (asm_simp_tac (FOL_ss addsimps [split]) 1);
+by (fast_tac (upair_cs addSEs [Pair_inject]) 1);
+val expand_split = result();
+
+
 (*** conversions for fst and snd ***)
 
 val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"