tuned names;
authorwenzelm
Wed Oct 25 18:33:01 2000 +0200 (2000-10-25)
changeset 10333f12ff6a4bc7b
parent 10332 b4f7f8693f8e
child 10334 e5e6070fcef5
tuned names;
src/HOL/Library/Quotient.thy
     1.1 --- a/src/HOL/Library/Quotient.thy	Wed Oct 25 18:32:40 2000 +0200
     1.2 +++ b/src/HOL/Library/Quotient.thy	Wed Oct 25 18:33:01 2000 +0200
     1.3 @@ -27,9 +27,9 @@
     1.4    eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
     1.5  
     1.6  axclass equiv < eqv
     1.7 -  eqv_refl [intro]: "x \<sim> x"
     1.8 -  eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
     1.9 -  eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
    1.10 +  equiv_refl [intro]: "x \<sim> x"
    1.11 +  equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
    1.12 +  equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
    1.13  
    1.14  text {*
    1.15   \medskip The quotient type @{text "'a quot"} consists of all