equal
deleted
inserted
replaced
19 text {* |
19 text {* |
20 \medskip Type class @{text equiv} models equivalence relations @{text |
20 \medskip Type class @{text equiv} models equivalence relations @{text |
21 "\<sim> :: 'a => 'a => bool"}. |
21 "\<sim> :: 'a => 'a => bool"}. |
22 *} |
22 *} |
23 |
23 |
24 class eqv = |
24 class eqv = type + |
25 fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>\<sim>" 50) |
25 fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>\<sim>" 50) |
26 |
26 |
27 class equiv = eqv + |
27 class equiv = eqv + |
28 assumes equiv_refl [intro]: "x \<^loc>\<sim> x" |
28 assumes equiv_refl [intro]: "x \<^loc>\<sim> x" |
29 assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z" |
29 assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z" |