--- a/src/HOL/Analysis/Change_Of_Vars.thy Fri Apr 12 22:24:07 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Fri Apr 12 22:24:57 2019 +0200
@@ -423,7 +423,7 @@
subsection\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>(*FIX ME mv *)
-(*https://en.wikipedia.org/wiki/F\<sigma>_set*)
+\<comment> \<open>\<^url>\<open>https://en.wikipedia.org/wiki/F\<sigma>_set\<close>\<close>
inductive\<^marker>\<open>tag important\<close> fsigma :: "'a::topological_space set \<Rightarrow> bool" where
"(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (\<Union>(F ` UNIV))"
--- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Fri Apr 12 22:24:07 2019 +0200
+++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Fri Apr 12 22:24:57 2019 +0200
@@ -7,7 +7,7 @@
text \<open>
The proof of the Generalised Binomial Theorem and related results.
We prove the generalised binomial theorem for complex numbers, following the proof at:
- \url{https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem}
+ \<^url>\<open>https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem\<close>
\<close>
theory Generalised_Binomial_Theorem
--- a/src/HOL/Analysis/Starlike.thy Fri Apr 12 22:24:07 2019 +0200
+++ b/src/HOL/Analysis/Starlike.thy Fri Apr 12 22:24:57 2019 +0200
@@ -7380,7 +7380,7 @@
by (metis (no_types) adjoint_works euclidean_eqI)
qed
-(*http://mathonline.wikidot.com/injectivity-and-surjectivity-of-the-adjoint-of-a-linear-map*)
+\<comment> \<open>\<^url>\<open>https://mathonline.wikidot.com/injectivity-and-surjectivity-of-the-adjoint-of-a-linear-map\<close>\<close>
lemma surj_adjoint_iff_inj [simp]:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
assumes "linear f"
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Fri Apr 12 22:24:07 2019 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Fri Apr 12 22:24:57 2019 +0200
@@ -174,7 +174,7 @@
An Elementary Proof of the Stone-Weierstrass Theorem.
Proceedings of the American Mathematical Society
Volume 81, Number 1, January 1981.
-DOI: 10.2307/2043993 https://www.jstor.org/stable/2043993\<close>
+DOI: 10.2307/2043993 \<^url>\<open>https://www.jstor.org/stable/2043993\<close>\<close>
locale function_ring_on =
fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"