# 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.