src/HOL/Library/Quotient.thy
changeset 25062 af5ef0d4d655
parent 23394 474ff28210c0
child 25594 43c718438f9f
     1.1 --- a/src/HOL/Library/Quotient.thy	Tue Oct 16 23:12:38 2007 +0200
     1.2 +++ b/src/HOL/Library/Quotient.thy	Tue Oct 16 23:12:45 2007 +0200
     1.3 @@ -22,12 +22,12 @@
     1.4  *}
     1.5  
     1.6  class eqv = type +
     1.7 -  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<^loc>\<sim>" 50)
     1.8 +  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
     1.9  
    1.10  class equiv = eqv +
    1.11 -  assumes equiv_refl [intro]: "x \<^loc>\<sim> x"
    1.12 -  assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z"
    1.13 -  assumes equiv_sym [sym]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> x"
    1.14 +  assumes equiv_refl [intro]: "x \<sim> x"
    1.15 +  assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
    1.16 +  assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
    1.17  
    1.18  lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    1.19  proof -