src/HOL/Imperative_HOL/Ref.thy
changeset 68224 1f7308050349
parent 67443 3abf6a722518
--- 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>