changeset 68224 | 1f7308050349 |
parent 68074 | 8d50467f7555 |
child 68607 | 67bb59e49834 |
--- a/src/HOL/Analysis/Linear_Algebra.thy Sat May 19 20:42:34 2018 +0200 +++ b/src/HOL/Analysis/Linear_Algebra.thy Sun May 20 11:57:17 2018 +0200 @@ -283,7 +283,7 @@ text \<open>TODO: The following lemmas about adjoints should hold for any Hilbert space (i.e. complete inner product space). - (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>) + (see \<^url>\<open>https://en.wikipedia.org/wiki/Hermitian_adjoint\<close>) \<close> lemma adjoint_works: