1.1 --- a/src/HOL/Analysis/L2_Norm.thy	Thu Dec 07 15:48:50 2017 +0100
     1.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Thu Dec 07 18:04:52 2017 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Complex_Main
     1.5  begin
     1.6  
     1.7 -definition "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
     1.8 +definition %important "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
     1.9  
    1.10  lemma L2_set_cong:
    1.11    "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
    1.12 @@ -73,9 +73,9 @@
    1.13    unfolding L2_set_def
    1.14    by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
    1.15  
    1.16 -lemma L2_set_triangle_ineq:
    1.17 -  shows "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
    1.18 -proof (cases "finite A")
    1.19 +lemma %important L2_set_triangle_ineq:
    1.20 +  "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
    1.21 +proof %unimportant (cases "finite A")
    1.22    case False
    1.23    thus ?thesis by simp
    1.24  next