src/HOL/Relation.ML
changeset 2031 03a843f0f447
parent 1985 84cf16192e03
child 2637 e9b203f854ae
     1.1 --- a/src/HOL/Relation.ML	Thu Sep 26 11:11:22 1996 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Sep 26 12:47:47 1996 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4  AddSEs [converseE];
     1.5  
     1.6  goalw Relation.thy [converse_def] "converse(converse R) = R";
     1.7 -by(Fast_tac 1);
     1.8 +by (Fast_tac 1);
     1.9  qed "converse_converse";
    1.10  
    1.11  (** Domain **)