--- a/src/HOL/Set.thy Mon Nov 05 17:48:51 2007 +0100
+++ b/src/HOL/Set.thy Mon Nov 05 18:18:39 2007 +0100
@@ -780,6 +780,8 @@
show "x \<notin> A - {x}" by blast
qed
+lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
+by auto
subsubsection {* Singletons, using insert *}