diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Dec 09 12:22:23 2013 +0100
@@ -1414,7 +1414,7 @@
 
 text {*
 Proof that Cauchy sequences converge based on the one from
-http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html
+@{url "http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html"}
 *}
 
 text {*