diff -r d7f5607fbadf -r b89e6cc963e3 src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Tue Nov 21 19:02:31 2000 +0100
+++ b/src/HOL/Library/Quotient.thy	Tue Nov 21 19:03:06 2000 +0100
@@ -185,7 +185,7 @@
   assume cong: "PROP ?cong"
   assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
-  also have "\<dots> = g a b"
+  also have "... = g a b"
   proof (rule cong)
     show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
     moreover