--- a/src/HOL/Analysis/Linear_Algebra.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Fri Aug 12 17:53:55 2016 +0200
@@ -1654,8 +1654,8 @@
qed
text \<open>TODO: The following lemmas about adjoints should hold for any
-Hilbert space (i.e. complete inner product space).
-(see @{url "http://en.wikipedia.org/wiki/Hermitian_adjoint"})
+ Hilbert space (i.e. complete inner product space).
+ (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
\<close>
lemma adjoint_works: