src/HOL/Library/Quotient.thy
 changeset 22390 378f34b1e380 parent 21404 eb85850d3eb7 child 22473 753123c89d72
```     1.1 --- a/src/HOL/Library/Quotient.thy	Fri Mar 02 15:43:20 2007 +0100
1.2 +++ b/src/HOL/Library/Quotient.thy	Fri Mar 02 15:43:21 2007 +0100
1.3 @@ -11,7 +11,7 @@
1.4
1.5  text {*
1.6   We introduce the notion of quotient types over equivalence relations
1.7 - via axiomatic type classes.
1.8 + via type classes.
1.9  *}
1.10
1.11  subsection {* Equivalence relations and quotient types *}
1.12 @@ -21,14 +21,13 @@
1.13   "\<sim> :: 'a => 'a => bool"}.
1.14  *}
1.15
1.16 -axclass eqv \<subseteq> type
1.17 -consts
1.18 -  eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
1.19 +class eqv =
1.20 +  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<^loc>\<sim>" 50)
1.21
1.22 -axclass equiv \<subseteq> eqv
1.23 -  equiv_refl [intro]: "x \<sim> x"
1.24 -  equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
1.25 -  equiv_sym [sym]: "x \<sim> y ==> y \<sim> x"
1.26 +class equiv = eqv +
1.27 +  assumes equiv_refl [intro]: "x \<^loc>\<sim> x"
1.28 +  assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z"
1.29 +  assumes equiv_sym [sym]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> x"
1.30
1.31  lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
1.32  proof -
```