# HG changeset patch
# User nipkow
# Date 1091639381 -7200
# Node ID 492e5f3a85717f5b7f897651ef9e79965bd33d03
# Parent  f233706d9fcea4ac203caa4c0d512307e1a4cb9c
added a few thms

diff -r f233706d9fce -r 492e5f3a8571 src/HOL/Integ/Equiv.thy
--- 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*}