Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new lemma
authorpaulson
Wed, 26 Feb 2003 10:44:54 +0100
changeset 13831 ab27b36aba99
parent 13830 7f8c1b533e8b
child 13832 e7649436869c
new lemma
src/HOL/Set.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle