summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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