equal
deleted
inserted
replaced
21 text {* |
21 text {* |
22 \medskip Type class @{text equiv} models equivalence relations @{text |
22 \medskip Type class @{text equiv} models equivalence relations @{text |
23 "\<sim> :: 'a => 'a => bool"}. |
23 "\<sim> :: 'a => 'a => bool"}. |
24 *} |
24 *} |
25 |
25 |
26 axclass eqv \<subseteq> "term" |
26 axclass eqv \<subseteq> type |
27 consts |
27 consts |
28 eqv :: "('a::eqv) => 'a => bool" (infixl "\<sim>" 50) |
28 eqv :: "('a::eqv) => 'a => bool" (infixl "\<sim>" 50) |
29 |
29 |
30 axclass equiv \<subseteq> eqv |
30 axclass equiv \<subseteq> eqv |
31 equiv_refl [intro]: "x \<sim> x" |
31 equiv_refl [intro]: "x \<sim> x" |