Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned names;
authorwenzelm
Wed, 25 Oct 2000 18:33:01 +0200
changeset 10333 f12ff6a4bc7b
parent 10332 b4f7f8693f8e
child 10334 e5e6070fcef5
tuned names;
src/HOL/Library/Quotient.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle