src/HOL/Library/Quotient.thy
changeset 10505 b89e6cc963e3
parent 10499 2f33d0fd242e
child 10551 ec9fab41b3a0
     1.1 --- a/src/HOL/Library/Quotient.thy	Tue Nov 21 19:02:31 2000 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Tue Nov 21 19:03:06 2000 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4    assume cong: "PROP ?cong"
     1.5    assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
     1.6    hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
     1.7 -  also have "\<dots> = g a b"
     1.8 +  also have "... = g a b"
     1.9    proof (rule cong)
    1.10      show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
    1.11      moreover