src/HOL/Relation.ML
changeset 4423 a129b817b58a
parent 4089 96fba19bcbe2
child 4593 6fc8f224655f
--- 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 **)