removed (un)important tags again to make latex happy
authornipkow
Wed Dec 06 16:01:15 2017 +0100 (10 months ago)
changeset 67144cef9a1514ed0
parent 67143 db609ac2c307
child 67150 ecbd8ff928c5
removed (un)important tags again to make latex happy
src/HOL/Analysis/L2_Norm.thy
     1.1 --- a/src/HOL/Analysis/L2_Norm.thy	Wed Dec 06 15:17:05 2017 +0100
     1.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Wed Dec 06 16:01:15 2017 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Complex_Main
     1.5  begin
     1.6  
     1.7 -definition %important
     1.8 +definition
     1.9    "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
    1.10  
    1.11  lemma setL2_cong:
    1.12 @@ -74,9 +74,9 @@
    1.13    unfolding setL2_def
    1.14    by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
    1.15  
    1.16 -lemma %important setL2_triangle_ineq:
    1.17 +lemma setL2_triangle_ineq:
    1.18    shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
    1.19 -proof %unimportant (cases "finite A")
    1.20 +proof (cases "finite A")
    1.21    case False
    1.22    thus ?thesis by simp
    1.23  next