diff -r 9752ba7348b5 -r 7bdfc1d6b143 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 22 11:34:57 2010 +0100
+++ b/src/HOL/List.thy	Mon Nov 22 11:34:58 2010 +0100
@@ -4877,6 +4877,10 @@
 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
 
+definition list_ex1
+where
+  list_ex1_iff: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
+
 text {*
   Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
   over @{const list_all} and @{const list_ex} in specifications.
@@ -4892,6 +4896,11 @@
   "list_ex P [] \<longleftrightarrow> False"
   by (simp_all add: list_ex_iff)
 
+lemma list_ex1_simps [simp, code]:
+  "list_ex1 P [] = False"
+  "list_ex1 P (x # xs) = (if P x then list_all (\<lambda>y. \<not> P y \<or> x = y) xs else list_ex1 P xs)"
+unfolding list_ex1_iff list_all_iff by auto
+
 lemma Ball_set_list_all [code_unfold]:
   "Ball (set xs) P \<longleftrightarrow> list_all P xs"
   by (simp add: list_all_iff)