src/HOL/Library/Quotient.thy
changeset 10333 f12ff6a4bc7b
parent 10311 3b53ed2c846f
child 10390 1d54567bed24
equal deleted inserted replaced
10332:b4f7f8693f8e 10333:f12ff6a4bc7b
    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)
    28 
    28 
    29 axclass equiv < eqv
    29 axclass equiv < eqv
    30   eqv_refl [intro]: "x \<sim> x"
    30   equiv_refl [intro]: "x \<sim> x"
    31   eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
    31   equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
    32   eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
    32   equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
    33 
    33 
    34 text {*
    34 text {*
    35  \medskip The quotient type @{text "'a quot"} consists of all
    35  \medskip The quotient type @{text "'a quot"} consists of all
    36  \emph{equivalence classes} over elements of the base type @{typ 'a}.
    36  \emph{equivalence classes} over elements of the base type @{typ 'a}.
    37 *}
    37 *}