diff -r a92a7f45ca28 -r 9591362629e3 src/HOL/Library/More_Set.thy
--- a/src/HOL/Library/More_Set.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Library/More_Set.thy	Mon Jun 28 15:32:06 2010 +0200
@@ -37,16 +37,8 @@
 subsection {* Basic set operations *}
 
 lemma is_empty_set:
-  "is_empty (set xs) \<longleftrightarrow> null xs"
-  by (simp add: is_empty_def null_empty)
-
-lemma ball_set:
-  "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
-  by (rule list_ball_code)
-
-lemma bex_set:
-  "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
-  by (rule list_bex_code)
+  "is_empty (set xs) \<longleftrightarrow> List.null xs"
+  by (simp add: is_empty_def null_def)
 
 lemma empty_set:
   "{} = set []"