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 -