# HG changeset patch
# User oheimb
# Date 882445858 -3600
# Node ID 41a7e4f0e957087d9d5a09c20e673cb38a872df3
# Parent  75f38104ff8063be64640af6d6938ac36195854f
added expand_split_asm

diff -r 75f38104ff80 -r 41a7e4f0e957 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Thu Dec 18 11:13:10 1997 +0100
+++ b/src/HOL/Prod.ML	Thu Dec 18 12:50:58 1997 +0100
@@ -173,7 +173,7 @@
 	(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
 
 (*For use with split_tac and the simplifier*)
-goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
+goal Prod.thy "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
 by (stac surjective_pairing 1);
 by (stac split 1);
 by (Blast_tac 1);
@@ -185,6 +185,11 @@
    the current goal contains one of those constants
 *)
 
+goal Prod.thy "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
+by (stac expand_split 1);
+by (Simp_tac 1);
+qed "expand_split_asm";
+
 (** split used as a logical connective or set former **)
 
 (*These rules are for use with blast_tac.