src/HOL/Library/Quotient.thy
changeset 10505 b89e6cc963e3
parent 10499 2f33d0fd242e
child 10551 ec9fab41b3a0
--- 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