--- a/src/HOL/Equiv_Relations.thy Fri Nov 19 17:52:07 2004 +0100
+++ b/src/HOL/Equiv_Relations.thy Sun Nov 21 12:52:03 2004 +0100
@@ -143,6 +143,15 @@
by(simp add: quotient_def)
+lemma singleton_quotient: "{x}//r = {r `` {x}}"
+by(simp add:quotient_def)
+
+lemma quotient_diff1:
+ "\<lbrakk> inj_on (%a. {a}//r) A; a \<in> A \<rbrakk> \<Longrightarrow> (A - {a})//r = A//r - {a}//r"
+apply(simp add:quotient_def inj_on_def)
+apply blast
+done
+
subsection {* Defining unary operations upon equivalence classes *}
text{*A congruence-preserving function*}