--- a/src/HOL/Finite_Set.thy Sat Feb 15 21:15:03 2020 +0100
+++ b/src/HOL/Finite_Set.thy Sun Feb 16 18:01:03 2020 +0100
@@ -1785,11 +1785,6 @@
obtains x where "A = {x}"
using assms by (auto simp: card_Suc_eq)
-lemma card_2_doubletonE:
- assumes "card A = Suc (Suc 0)"
- obtains x y where "A = {x,y}" "x\<noteq>y"
- using assms by (blast dest: card_eq_SucD)
-
lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
unfolding is_singleton_def
by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)