src/HOL/Integ/Equiv.thy

   apply (rule iffI)  
    prefer 2 apply (blast del: equalityI intro: quotient_eqI) 
   apply (clarify elim!: quotientE)
   apply (unfold equiv_def sym_def trans_def, blast)
   done
+
+
+lemma quotient_empty [simp]: "{}//r = {}"
+by(simp add: quotient_def)
+
+lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})"
+by(simp add: quotient_def)
+
+lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})"
+by(simp add: quotient_def)
 
 
 subsection {* Defining unary operations upon equivalence classes *}
 
 text{*A congruence-preserving function*}