diff -r 7538b5f301ea -r 16d98ef49a2c src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Wed Jul 18 17:01:12 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Tue Jul 17 12:23:37 2018 +0200
@@ -86,14 +86,14 @@
 
 
 
-definition abs_summable_on ::
+definition%important abs_summable_on ::
     "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" 
     (infix "abs'_summable'_on" 50)
  where
    "f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"
 
 
-definition infsetsum ::
+definition%important infsetsum ::
     "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> 'b"
  where
    "infsetsum f A = lebesgue_integral (count_space A) f"
@@ -553,7 +553,7 @@
        (insert assms, auto simp: bij_betw_def)    
 qed
 
-lemma infsetsum_reindex:
+theorem infsetsum_reindex:
   assumes "inj_on g A"
   shows   "infsetsum f (g ` A) = infsetsum (\<lambda>x. f (g x)) A"
   by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms)
@@ -607,7 +607,7 @@
   unfolding abs_summable_on_def infsetsum_def
   by (rule Bochner_Integration.integral_norm_bound)
 
-lemma infsetsum_Sigma:
+theorem infsetsum_Sigma:
   fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
   assumes [simp]: "countable A" and "\<And>i. countable (B i)"
   assumes summable: "f abs_summable_on (Sigma A B)"
@@ -692,7 +692,7 @@
   finally show ?thesis .
 qed
 
-lemma abs_summable_on_Sigma_iff:
+theorem abs_summable_on_Sigma_iff:
   assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
   shows   "f abs_summable_on Sigma A B \<longleftrightarrow> 
              (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
@@ -783,7 +783,7 @@
   by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]]
         norm_infsetsum_bound)
 
-lemma infsetsum_prod_PiE:
+theorem infsetsum_prod_PiE:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
   assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
   assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"