src/HOL/Relation.ML
changeset 1552 6f71b5d46700
parent 1465 5d7a7e439cec
child 1605 248e1e125ca0
     1.1 --- a/src/HOL/Relation.ML	Wed Mar 06 12:19:16 1996 +0100
     1.2 +++ b/src/HOL/Relation.ML	Wed Mar 06 12:52:11 1996 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  qed "idE";
     1.5  
     1.6  goalw Relation.thy [id_def] "(a,b):id = (a=b)";
     1.7 -by(fast_tac prod_cs 1);
     1.8 +by (fast_tac prod_cs 1);
     1.9  qed "pair_in_id_conv";
    1.10  
    1.11