--- a/src/HOL/Finite_Set.thy Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Finite_Set.thy Wed Sep 18 14:41:37 2019 +0100
@@ -1493,12 +1493,11 @@
using card_Un_Int [of A B] by simp
lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
- apply (cases "finite A")
- apply (cases "finite B")
- apply (use le_iff_add card_Un_Int in blast)
- apply simp
- apply simp
- done
+proof (cases "finite A \<and> finite B")
+ case True
+ then show ?thesis
+ using le_iff_add card_Un_Int [of A B] by auto
+qed auto
lemma card_Diff_subset:
assumes "finite B"