src/HOL/Series.thy
changeset 54703 499f92dc6e45
parent 54230 b1d955791529
child 56178 2a6f58938573
     1.1 --- a/src/HOL/Series.thy	Mon Dec 09 12:16:52 2013 +0100
     1.2 +++ b/src/HOL/Series.thy	Mon Dec 09 12:22:23 2013 +0100
     1.3 @@ -719,8 +719,10 @@
     1.4  
     1.5  subsection {* Cauchy Product Formula *}
     1.6  
     1.7 -(* Proof based on Analysis WebNotes: Chapter 07, Class 41
     1.8 -http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm *)
     1.9 +text {*
    1.10 +  Proof based on Analysis WebNotes: Chapter 07, Class 41
    1.11 +  @{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
    1.12 +*}
    1.13  
    1.14  lemma setsum_triangle_reindex:
    1.15    fixes n :: nat