--- a/src/HOL/Integ/Equiv.thy Wed Aug 04 17:43:55 2004 +0200
+++ b/src/HOL/Integ/Equiv.thy Wed Aug 04 19:09:41 2004 +0200
@@ -132,6 +132,16 @@
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*}