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