--- a/src/HOL/Imperative_HOL/Ref.thy Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Sun May 20 11:57:17 2018 +0200
@@ -10,8 +10,8 @@
text \<open>
Imperative reference operations; modeled after their ML counterparts.
- See \<^url>\<open>http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
- and \<^url>\<open>http://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
+ See \<^url>\<open>https://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
+ and \<^url>\<open>https://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
\<close>
subsection \<open>Primitives\<close>