merged

--- a/src/Doc/manual.bib	Sun Feb 11 15:13:40 2018 +0100
+++ b/src/Doc/manual.bib	Sun Feb 11 22:26:58 2018 +0100
@@ -169,7 +169,7 @@
   volume = 52,
   number = 2,
   pages = {123--153},
-  url = {http://dx.doi.org/10.1007/s10817-013-9284-7},
+  url = {https://doi.org/10.1007/s10817-013-9284-7},
   year = {2014}}
 
 @InCollection{Barendregt-Geuvers:2001,
@@ -655,7 +655,7 @@
   number    = {3},
   pages     = {267--286},
   year      = {2008},
-  url       = {http://dx.doi.org/10.1016/j.jal.2007.11.001},
+  url       = {https://doi.org/10.1016/j.jal.2007.11.001},
 }
 
 @InProceedings{felty91a,
@@ -1085,7 +1085,7 @@
   booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP}
                2015, Nanjing, China, August 24-27, 2015, Proceedings},
   year      = {2015},
-  url       = {http://dx.doi.org/10.1007/978-3-319-22102-1_16},
+  url       = {https://doi.org/10.1007/978-3-319-22102-1_16},
   series    = {Lecture Notes in Computer Science},
   volume    = {9236},
   publisher = {Springer},
@@ -1182,7 +1182,7 @@
                2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
                Austria},
   year      = {2014},
-  url       = {http://dx.doi.org/10.1007/978-3-319-08970-6_25},
+  url       = {https://doi.org/10.1007/978-3-319-08970-6_25},
   doi       = {10.1007/978-3-319-08970-6_25},
   series    = "LNCS",
   volume    = {8558},
@@ -2154,7 +2154,7 @@
                Christine Paulin-Mohring and
                David Pichardie},
   year      = {2013},
-  ee        = {http://dx.doi.org/10.1007/978-3-642-39634-2_30},
+  ee        = {https://doi.org/10.1007/978-3-642-39634-2_30},
   publisher = {Springer},
   series    = {Lecture Notes in Computer Science},
   volume    = {7998},

--- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Feb 11 15:13:40 2018 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sun Feb 11 22:26:58 2018 +0100
@@ -1571,7 +1571,7 @@
   Proof that @{const rel_pmf} preserves orders.
   Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
   Theoretical Computer Science 12(1):19--37, 1980,
-  \<^url>\<open>http://dx.doi.org/10.1016/0304-3975(80)90003-1\<close>
+  \<^url>\<open>https://doi.org/10.1016/0304-3975(80)90003-1\<close>
 \<close>
 
 lemma

--- a/src/Tools/Graphview/layout.scala	Sun Feb 11 15:13:40 2018 +0100
+++ b/src/Tools/Graphview/layout.scala	Sun Feb 11 22:26:58 2018 +0100
@@ -7,7 +7,7 @@
   Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing,
   DIMACS International Workshop (GD'94), Springer LNCS 894, 1995.
 
-  http://dx.doi.org/10.1007/3-540-58950-3_371
+  https://doi.org/10.1007/3-540-58950-3_371
   ftp://ftp.cs.uni-sb.de/pub/graphics/vcg/doc/tr-A03-94.ps.gz
 */