# HG changeset patch
# User paulson
# Date 1046252694 -3600
# Node ID ab27b36aba99689ef4db7275243f2f549655477e
# Parent  7f8c1b533e8b254a35947006ea945bbe564f0398
new lemma

diff -r 7f8c1b533e8b -r ab27b36aba99 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Feb 26 10:44:16 2003 +0100
+++ b/src/HOL/Set.thy	Wed Feb 26 10:44:54 2003 +0100
@@ -1647,6 +1647,9 @@
 lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
   by blast
 
+lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
+  by blast
+
 lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
   by rules