| changeset 5600 | 34b3366b83ac |
| parent 5521 | 7970832271cc |
| child 5649 | 1bac26652f45 |
--- a/src/HOL/Set.ML Thu Oct 01 18:29:38 1998 +0200 +++ b/src/HOL/Set.ML Thu Oct 01 18:29:53 1998 +0200 @@ -460,6 +460,11 @@ qed "singleton_conv"; Addsimps [singleton_conv]; +Goal "{x. a=x} = {a}"; +by(Blast_tac 1); +qed "singleton_conv2"; +Addsimps [singleton_conv2]; + section "Unions of families -- UNION x:A. B(x) is Union(B``A)";