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

src/HOL/Library/Quotient.thy

changeset 10286 | fdcdb8a80988 |

parent 10285 | 6949e17f314a |

child 10311 | 3b53ed2c846f |

1.1 --- a/src/HOL/Library/Quotient.thy Sun Oct 22 22:18:40 2000 +0200 1.2 +++ b/src/HOL/Library/Quotient.thy Sun Oct 22 22:23:16 2000 +0200 1.3 @@ -70,8 +70,8 @@ 1.4 subsection {* Equality on quotients *} 1.5 1.6 text {* 1.7 - Equality of canonical quotient elements corresponds to the original 1.8 - relation as follows. 1.9 + Equality of canonical quotient elements coincides with the original 1.10 + relation. 1.11 *} 1.12 1.13 theorem equivalence_class_eq [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"