# HG changeset patch
# User wenzelm
# Date 972491581 -7200
# Node ID f12ff6a4bc7bea6fada90d5029bf1d956c09ee27
# Parent  b4f7f8693f8e3e86c89ee9d7d6ad60a10220bb5a
tuned names;

diff -r b4f7f8693f8e -r f12ff6a4bc7b src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Wed Oct 25 18:32:40 2000 +0200
+++ b/src/HOL/Library/Quotient.thy	Wed Oct 25 18:33:01 2000 +0200
@@ -27,9 +27,9 @@
   eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
 
 axclass equiv < eqv
-  eqv_refl [intro]: "x \<sim> x"
-  eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
-  eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
+  equiv_refl [intro]: "x \<sim> x"
+  equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
+  equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
 
 text {*
  \medskip The quotient type @{text "'a quot"} consists of all