author | nipkow |
Wed, 29 Nov 2000 17:24:20 +0100 | |
changeset 10540 | abe2322fa422 |
parent 10539 | 5929460a41df |
child 10541 | fdec07d4f047 |
--- 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 **)