src/HOL/Analysis/Linear_Algebra.thy
changeset 63680 6e1e8b5abbfa
parent 63627 6ddb43c6b711
child 63881 b746b19197bd
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Aug 12 17:49:02 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Aug 12 17:53:55 2016 +0200
     1.3 @@ -1654,8 +1654,8 @@
     1.4  qed
     1.5  
     1.6  text \<open>TODO: The following lemmas about adjoints should hold for any
     1.7 -Hilbert space (i.e. complete inner product space).
     1.8 -(see @{url "http://en.wikipedia.org/wiki/Hermitian_adjoint"})
     1.9 +  Hilbert space (i.e. complete inner product space).
    1.10 +  (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
    1.11  \<close>
    1.12  
    1.13  lemma adjoint_works: