--- a/src/HOL/Relation.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Relation.ML Tue Dec 16 17:58:03 1997 +0100
@@ -109,7 +109,7 @@
Addsimps [inverse_inverse];
goal Relation.thy "(r O s)^-1 = s^-1 O r^-1";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "inverse_comp";
(** Domain **)