| changeset 63680 | 6e1e8b5abbfa |
| parent 63556 | 36e9732988ce |
| child 63915 | bab633745c7f |
--- a/src/HOL/Real_Vector_Spaces.thy Fri Aug 12 17:49:02 2016 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Fri Aug 12 17:53:55 2016 +0200 @@ -2084,7 +2084,7 @@ 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>