src/HOL/Factorial.thy

--- a/src/HOL/Factorial.thy	Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Factorial.thy	Sun May 20 11:57:17 2018 +0200
@@ -182,7 +182,7 @@
 
 subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>
 
-text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
+text \<open>See \<^url>\<open>https://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
 
 context comm_semiring_1
 begin