equal
deleted
inserted
replaced
16 *} |
16 *} |
17 |
17 |
18 subsection {* Equivalence relations and quotient types *} |
18 subsection {* Equivalence relations and quotient types *} |
19 |
19 |
20 text {* |
20 text {* |
21 \medskip Type class @{text equiv} models equivalence relations using |
21 \medskip Type class @{text equiv} models equivalence relations @{text |
22 the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation. |
22 "\<sim> :: 'a => 'a => bool"}. |
23 *} |
23 *} |
24 |
24 |
25 axclass eqv < "term" |
25 axclass eqv < "term" |
26 consts |
26 consts |
27 eqv :: "('a::eqv) => 'a => bool" (infixl "\<sim>" 50) |
27 eqv :: "('a::eqv) => 'a => bool" (infixl "\<sim>" 50) |