src/HOL/Set.thy

--- a/src/HOL/Set.thy	Wed Sep 26 20:27:57 2007 +0200
+++ b/src/HOL/Set.thy	Wed Sep 26 20:27:58 2007 +0200
@@ -771,6 +771,15 @@
 lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"
   by auto
 
+lemma set_insert:
+  assumes "x \<in> A"
+  obtains B where "A = insert x B" and "x \<notin> B"
+proof
+  from assms show "A = insert x (A - {x})" by blast
+next
+  show "x \<notin> A - {x}" by blast
+qed
+
 
 subsubsection {* Singletons, using insert *}