src/HOL/Set.ML
changeset 6301 08245f5a436d
parent 6291 2c3f72d9f5d1
child 6394 3d9fd50fcc43
     1.1 --- a/src/HOL/Set.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/Set.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -467,7 +467,7 @@
     1.4  Addsimps [singleton_conv];
     1.5  
     1.6  Goal "{x. a=x} = {a}";
     1.7 -by(Blast_tac 1);
     1.8 +by (Blast_tac 1);
     1.9  qed "singleton_conv2";
    1.10  Addsimps [singleton_conv2];
    1.11