--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Sun May 20 11:57:17 2018 +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 http://www.jstor.org/stable/2043993\<close>
+DOI: 10.2307/2043993 https://www.jstor.org/stable/2043993\<close>
locale function_ring_on =
fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"