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