# HG changeset patch
# User nipkow
# Date 1512666292 -3600
# Node ID 3a9966b88a5082f9be25d39f0d290312d2510774
# Parent  9e5b05d54f9dc28c6c3b2da54067e9f429ee8b8c
"important" annotations

diff -r 9e5b05d54f9d -r 3a9966b88a50 src/HOL/Analysis/L2_Norm.thy
--- a/src/HOL/Analysis/L2_Norm.thy	Thu Dec 07 15:48:50 2017 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy	Thu Dec 07 18:04:52 2017 +0100
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-definition "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
+definition %important "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
 
 lemma L2_set_cong:
   "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
@@ -73,9 +73,9 @@
   unfolding L2_set_def
   by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
 
-lemma L2_set_triangle_ineq:
-  shows "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
-proof (cases "finite A")
+lemma %important L2_set_triangle_ineq:
+  "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
+proof %unimportant (cases "finite A")
   case False
   thus ?thesis by simp
 next