src/HOL/Real_Vector_Spaces.thy
changeset 54703 499f92dc6e45
parent 54489 03ff4d1e6784
child 54778 13f08c876899
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Dec 09 12:16:52 2013 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Dec 09 12:22:23 2013 +0100
     1.3 @@ -1414,7 +1414,7 @@
     1.4  
     1.5  text {*
     1.6  Proof that Cauchy sequences converge based on the one from
     1.7 -http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html
     1.8 +@{url "http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html"}
     1.9  *}
    1.10  
    1.11  text {*