src/HOL/Real_Vector_Spaces.thy

 
 subsection \<open>The set of real numbers is a complete metric space\<close>
 
 text \<open>
   Proof that Cauchy sequences converge based on the one from
-  @{url "http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html"}
+  \<^url>\<open>http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html\<close>
 \<close>
 
 text \<open>
   If sequence @{term "X"} is Cauchy, then its limit is the lub of
   @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"}