src/ZF/ex/Integ.ML

--- a/src/ZF/ex/Integ.ML	Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/ex/Integ.ML	Thu Aug 06 12:24:04 1998 +0200
@@ -286,8 +286,7 @@
 
 (** Congruence property for multiplication **)
 
-Goal 
-    "congruent2(intrel, %p1 p2.                 \
+Goal "congruent2(intrel, %p1 p2.                 \
 \               split(%x1 y1. split(%x2 y2.     \
 \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
 by (rtac (equiv_intrel RS congruent2_commuteI) 1);