new lemma
authorpaulson
Wed Feb 26 10:44:54 2003 +0100 (2003-02-26)
changeset 13831ab27b36aba99
parent 13830 7f8c1b533e8b
child 13832 e7649436869c
new lemma
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Wed Feb 26 10:44:16 2003 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Feb 26 10:44:54 2003 +0100
     1.3 @@ -1647,6 +1647,9 @@
     1.4  lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
     1.5    by blast
     1.6  
     1.7 +lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
     1.8 +  by blast
     1.9 +
    1.10  lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
    1.11    by rules
    1.12