--- a/src/HOL/Analysis/L2_Norm.thy Wed Dec 06 15:17:05 2017 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy Wed Dec 06 16:01:15 2017 +0100
@@ -8,7 +8,7 @@
imports Complex_Main
begin
-definition %important
+definition
"setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
lemma setL2_cong:
@@ -74,9 +74,9 @@
unfolding setL2_def
by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
-lemma %important setL2_triangle_ineq:
+lemma setL2_triangle_ineq:
shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
-proof %unimportant (cases "finite A")
+proof (cases "finite A")
case False
thus ?thesis by simp
next