| changeset 54703 | 499f92dc6e45 |
| parent 54489 | 03ff4d1e6784 |
| child 54778 | 13f08c876899 |
--- 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 {*