# HG changeset patch
# User wenzelm
# Date 1003343043 -7200
# Node ID 015a82d4ee963a071a088bd1268bc21371fe8cbf
# Parent  9283b3c11234863afe434e4ded7b4a5b9a3cb991
proper proof of split_paired_all (presently unused);

diff -r 9283b3c11234 -r 015a82d4ee96 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 17 18:52:30 2001 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 17 20:24:03 2001 +0200
@@ -115,6 +115,18 @@
 
 use "Product_Type_lemmas.ML"
 
+lemma (*split_paired_all:*) "(!!x. PROP P x) == (!!a b. PROP P (a, b))"   (* FIXME unused *)
+proof
+  fix a b
+  assume "!!x. PROP P x"
+  thus "PROP P (a, b)" .
+next
+  fix x
+  assume "!!a b. PROP P (a, b)"
+  hence "PROP P (fst x, snd x)" .
+  thus "PROP P x" by simp
+qed
+
 lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
   apply (rule_tac x = "(a, b)" in image_eqI)
    apply auto