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