summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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