# HG changeset patch
# User nipkow
# Date 1512572475 -3600
# Node ID cef9a1514ed0a2b3fa99c727393d21d315cd0398
# Parent  db609ac2c3073683b06fdf03aff96dd5f391c622
removed (un)important tags again to make latex happy

diff -r db609ac2c307 -r cef9a1514ed0 src/HOL/Analysis/L2_Norm.thy
--- 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