unsymbolize;
authorwenzelm
Tue Nov 21 19:03:06 2000 +0100 (2000-11-21)
changeset 10505b89e6cc963e3
parent 10504 d7f5607fbadf
child 10506 01333dbe1431
unsymbolize;
src/HOL/Library/Quotient.thy
     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