# HG changeset patch
# User nipkow
# Date 975515060 -3600
# Node ID abe2322fa422b102bf36e811b8d574f2891889b7
# Parent  5929460a41dfe6c3fabb80ec0f8a90a0b17285cd
expand_split_asm -> split_split_asm

diff -r 5929460a41df -r abe2322fa422 src/HOL/Product_Type.ML
--- a/src/HOL/Product_Type.ML	Wed Nov 29 17:23:27 2000 +0100
+++ b/src/HOL/Product_Type.ML	Wed Nov 29 17:24:20 2000 +0100
@@ -275,7 +275,7 @@
 Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
 by (stac split_split 1);
 by (Simp_tac 1);
-qed "expand_split_asm";
+qed "split_split_asm";
 
 (** split used as a logical connective or set former **)