--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Tue Mar 31 15:51:15 2020 +0200
@@ -154,7 +154,7 @@
lemma abs_summable_on_altdef':
"A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f"
unfolding abs_summable_on_def set_integrable_def
- by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset set_integrable_def sets_count_space space_count_space)
+ by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset sets_count_space space_count_space)
lemma abs_summable_on_norm_iff [simp]:
"(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"