--- a/src/HOL/Finite_Set.thy Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Finite_Set.thy Mon Oct 26 23:41:27 2015 +0000
@@ -1545,6 +1545,10 @@
apply(auto simp add: intro:ccontr)
done
+lemma card_1_singletonE:
+ assumes "card A = 1" obtains x where "A = {x}"
+ using assms by (auto simp: card_Suc_eq)
+
lemma card_le_Suc_iff: "finite A \<Longrightarrow>
Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff