| changeset 69593 | 3dda49e08b9d |
| parent 69587 | 53982d5ec0bb |
| child 76213 | e44d86131648 |
--- a/src/ZF/EquivClass.thy Fri Jan 04 21:49:06 2019 +0100 +++ b/src/ZF/EquivClass.thy Fri Jan 04 23:22:53 2019 +0100 @@ -31,7 +31,7 @@ subsection\<open>Suppes, Theorem 70: - @{term r} is an equiv relation iff @{term "converse(r) O r = r"}\<close> + \<^term>\<open>r\<close> is an equiv relation iff \<^term>\<open>converse(r) O r = r\<close>\<close> (** first half: equiv(A,r) ==> converse(r) O r = r **)