# HG changeset patch
# User wenzelm
# Date 1531925041 -7200
# Node ID f849fc1cb65e1fe2be41b952b05408b24aa85c0c
# Parent  371e814af6f048d9746d855785d49b4d9c6329bb
prefer HTTPS;

diff -r 371e814af6f0 -r f849fc1cb65e Admin/components/README
--- a/Admin/components/README	Wed Jul 18 12:21:55 2018 +0200
+++ b/Admin/components/README	Wed Jul 18 16:44:01 2018 +0200
@@ -38,7 +38,7 @@
 
 Isabelle components are managed as authentic .tar.gz archives in
 /home/isabelle/components from where they are made publicly available
-on http://isabelle.in.tum.de/components/.
+on https://isabelle.in.tum.de/components/.
 
 Visibility on the HTTP server depends on local Unix file permission:
 nonfree components should omit "read" mode for the Unix group/other;
diff -r 371e814af6f0 -r f849fc1cb65e README
--- a/README	Wed Jul 18 12:21:55 2018 +0200
+++ b/README	Wed Jul 18 16:44:01 2018 +0200
@@ -34,10 +34,10 @@
    The Isabelle home page may be accessed from the following mirror
    sites:
 
-     * http://www.cl.cam.ac.uk/research/hvg/Isabelle
-     * http://isabelle.in.tum.de
+     * https://www.cl.cam.ac.uk/research/hvg/Isabelle
+     * https://isabelle.in.tum.de
      * http://mirror.cse.unsw.edu.au/pub/isabelle
-     * http://mirror.clarkson.edu/isabelle
+     * https://mirror.clarkson.edu/isabelle
 
   Mailing list
 
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/How_to_Prove_it/document/root.bib
--- a/src/Doc/How_to_Prove_it/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/How_to_Prove_it/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
@@ -3,12 +3,12 @@
 @string{Springer="Springer-Verlag"}
 
 @manual{Main,author={Tobias Nipkow},title={What's in Main},
-note={\url{http://isabelle.in.tum.de/doc/main.pdf}}}
+note={\url{https://isabelle.in.tum.de/doc/main.pdf}}}
 
 @manual{ProgProve,author={Tobias Nipkow},
 title={Programming and Proving in Isabelle/HOL},
-note={\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}}
+note={\url{https://isabelle.in.tum.de/doc/prog-prove.pdf}}}
 
 @manual{IsarRef,author={Makarius Wenzel},
 title={The Isabelle/Isar Reference Manual},
-note={\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
+note={\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/Locales/document/root.bib
--- a/src/Doc/Locales/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/Locales/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
@@ -1,7 +1,7 @@
 @unpublished{IsarRef,
   author = "Markus Wenzel",
   title = "The {Isabelle/Isar} Reference Manual",
-  note = "Part of the Isabelle distribution, \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}."
+  note = "Part of the Isabelle distribution, \url{https://isabelle.in.tum.de/doc/isar-ref.pdf}."
 }
 
 @book {Jacobson1985,
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/Logics/document/preface.tex
--- a/src/Doc/Logics/document/preface.tex	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/Logics/document/preface.tex	Wed Jul 18 16:44:01 2018 +0200
@@ -56,7 +56,7 @@
 \begin{center}\small
   \begin{tabular}{l}
     \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
-    \url{http://isabelle.in.tum.de/library/} \\
+    \url{https://isabelle.in.tum.de/library/} \\
   \end{tabular}
 \end{center}
 
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/Prog_Prove/document/intro-isabelle.tex
--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex	Wed Jul 18 16:44:01 2018 +0200
@@ -56,7 +56,7 @@
 
 If you have not done so already, download and install Isabelle
 (this book is compatible with Isabelle2016-1)
-from \url{http://isabelle.in.tum.de}. You can start it by clicking
+from \url{https://isabelle.in.tum.de}. You can start it by clicking
 on the application icon. This will launch Isabelle's
 user interface based on the text editor \concept{jEdit}. Below you see
 a typical example snapshot of a session. At this point we merely explain
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/Prog_Prove/document/root.bib
--- a/src/Doc/Prog_Prove/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/Prog_Prove/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
@@ -13,10 +13,10 @@
 
 @manual{Krauss,author={Alexander Krauss},
 title={Defining Recursive Functions in Isabelle/HOL},
-note={\url{http://isabelle.in.tum.de/doc/functions.pdf}}}
+note={\url{https://isabelle.in.tum.de/doc/functions.pdf}}}
 
 @manual{Nipkow-Main,author={Tobias Nipkow},title={What's in Main},
-note={\url{http://isabelle.in.tum.de/doc/main.pdf}}}
+note={\url{https://isabelle.in.tum.de/doc/main.pdf}}}
 
 @book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
 title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
@@ -28,4 +28,4 @@
 
 @manual{IsarRef,author={Makarius Wenzel},
 title={The Isabelle/Isar Reference Manual},
-note={\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
+note={\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jul 18 16:44:01 2018 +0200
@@ -13,7 +13,7 @@
 %\usepackage[scaled=.85]{beramono}
 \usepackage{isabelle,iman,pdfsetup}
 
-\newcommand\download{\url{http://isabelle.in.tum.de/components/}}
+\newcommand\download{\url{https://isabelle.in.tum.de/components/}}
 
 \let\oldS=\S
 \def\S{\oldS\,}
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/Sugar/document/root.bib
--- a/src/Doc/Sugar/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/Sugar/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
@@ -8,5 +8,5 @@
 
 @misc{tar,author={Gerwin Klein and Norber Schirmer and Tobias Nipkow},
 title={{LaTeX} sugar theories and support files}, 
-note={\url{http://isabelle.in.tum.de/sugar.tar.gz}}}
+note={\url{https://isabelle.in.tum.de/sugar.tar.gz}}}
 
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/Tutorial/document/basics.tex
--- a/src/Doc/Tutorial/document/basics.tex	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/Tutorial/document/basics.tex	Wed Jul 18 16:44:01 2018 +0200
@@ -85,7 +85,7 @@
 \end{warn}
 HOL's theory collection is available online at
 \begin{center}\small
-    \url{http://isabelle.in.tum.de/library/HOL/}
+    \url{https://isabelle.in.tum.de/library/HOL/}
 \end{center}
 and is recommended browsing. In subdirectory \texttt{Library} you find
 a growing library of useful theories that are not part of \isa{Main}
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/Tutorial/document/fp.tex
--- a/src/Doc/Tutorial/document/fp.tex	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/Tutorial/document/fp.tex	Wed Jul 18 16:44:01 2018 +0200
@@ -130,7 +130,7 @@
 Lists are one of the essential datatypes in computing.  We expect that you
 are already familiar with their basic operations.
 Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
-\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
+\thydx{List}\footnote{\url{https://isabelle.in.tum.de/library/HOL/List.html}}.
 The latter contains many further operations. For example, the functions
 \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
 element and the remainder of a list. (However, pattern matching is usually
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/Tutorial/document/preface.tex
--- a/src/Doc/Tutorial/document/preface.tex	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/Tutorial/document/preface.tex	Wed Jul 18 16:44:01 2018 +0200
@@ -35,7 +35,7 @@
 from output generated in this way.  The final chapter of Part~I explains how
 users may produce their own formal documents in a similar fashion.
 
-Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains
+Isabelle's \hfootref{https://isabelle.in.tum.de/}{web site} contains
 links to the download area and to documentation and other information.
 The classic Isabelle user interface is Proof~General~/ Emacs by David
 Aspinall's\index{Aspinall, David}.  This book says very little about
diff -r 371e814af6f0 -r f849fc1cb65e src/Doc/manual.bib
--- a/src/Doc/manual.bib	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/Doc/manual.bib	Wed Jul 18 16:44:01 2018 +0200
@@ -158,7 +158,7 @@
   author        = {Clemens Ballarin},
   title         = {Tutorial to Locales and Locale Interpretation},
   institution   = TUM,
-  note          = {\url{http://isabelle.in.tum.de/doc/locales.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/locales.pdf}}
 }
 
 @article{Ballarin2014,
@@ -226,7 +226,7 @@
                   Markus Wenzel},
   title =        {The Supplemental {Isabelle/HOL} Library},
   note =         {Part of the Isabelle distribution,
-                  \url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
+                  \url{https://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
   year =         2002
 }
 
@@ -311,7 +311,7 @@
   author	= {Julian Biendarra and Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel},
   title		= {Defining (Co)datatypes and Primitively (Co)recursive Functions in {Isabelle\slash HOL}},
   institution	= {TU Munich},
-  note          = {\url{http://isabelle.in.tum.de/doc/datatypes.pdf}}}
+  note          = {\url{https://isabelle.in.tum.de/doc/datatypes.pdf}}}
 
 @book{Bird-Wadler,author="Richard Bird and Philip Wadler",
 title="Introduction to Functional Programming",publisher=PH,year=1988}
@@ -324,21 +324,21 @@
   author        = {Jasmin Christian Blanchette},
   title         = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle\slash {HOL}},
   institution   = TUM,
-  note          = {\url{http://isabelle.in.tum.de/doc/nitpick.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/nitpick.pdf}}
 }
 
 @manual{isabelle-sledgehammer,
   author        = {Jasmin Christian Blanchette},
   title         = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle\slash {HOL}},
   institution   = TUM,
-  note          = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/sledgehammer.pdf}}
 }
 
 @manual{isabelle-corec,
   author	= {Jasmin Christian Blanchette and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel},
   title		= {Defining Nonprimitively Corecursive Functions in {Isabelle\slash HOL}},
   institution	= {TU Munich},
-  note          = {\url{http://isabelle.in.tum.de/doc/corec.pdf}}}
+  note          = {\url{https://isabelle.in.tum.de/doc/corec.pdf}}}
 
 @inproceedings{blanchette-nipkow-2010,
   title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
@@ -831,14 +831,14 @@
   author        = {Florian Haftmann},
   title         = {Haskell-style type classes with {Isabelle}/{Isar}},
   institution   = TUM,
-  note          = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/classes.pdf}}
 }
 
 @manual{isabelle-codegen,
   author        = {Florian Haftmann},
   title         = {Code generation from Isabelle theories},
   institution   = TUM,
-  note          = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/codegen.pdf}}
 }
 
 @Book{halmos60,
@@ -1064,7 +1064,7 @@
   author        = {Alexander Krauss},
   title         = {Defining Recursive Functions in {Isabelle/HOL}},
   institution   = TUM,
-  note          = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/functions.pdf}}
 }
 
 @inproceedings{Kuncar:2015,
@@ -1366,7 +1366,7 @@
   title		= {{Isabelle}'s Logics: {HOL}},
   institution	= {Institut f{\"u}r Informatik, Technische Universi{\"a}t
                   M{\"u}nchen and Computer Laboratory, University of Cambridge},
-  note          = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
+  note          = {\url{https://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
 
 @article{nipkow-prehofer,
   author	= {Tobias Nipkow and Christian Prehofer},
@@ -1502,25 +1502,25 @@
   author	= {Lawrence C. Paulson},
   title		= {Old Introduction to {Isabelle}},
   institution	= CUCL,
-  note          = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}}
+  note          = {\url{https://isabelle.in.tum.de/doc/intro.pdf}}}
 
 @manual{isabelle-logics,
   author	= {Lawrence C. Paulson},
   title		= {{Isabelle's} Logics},
   institution	= CUCL,
-  note          = {\url{http://isabelle.in.tum.de/doc/logics.pdf}}}
+  note          = {\url{https://isabelle.in.tum.de/doc/logics.pdf}}}
 
 @manual{isabelle-ref,
   author	= {Lawrence C. Paulson},
   title		= {The Old {Isabelle} Reference Manual},
   institution	= CUCL,
-  note          = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}}
+  note          = {\url{https://isabelle.in.tum.de/doc/ref.pdf}}}
 
 @manual{isabelle-ZF,
   author	= {Lawrence C. Paulson},
   title		= {{Isabelle}'s Logics: {FOL} and {ZF}},
   institution	= CUCL,
-  note          = {\url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}}}
+  note          = {\url{https://isabelle.in.tum.de/doc/logics-ZF.pdf}}}
 
 @article{paulson-found,
   author	= {Lawrence C. Paulson},
@@ -2024,22 +2024,22 @@
 @manual{isabelle-system,
   author = {Makarius Wenzel},
   title = {The {Isabelle} System Manual},
-  note = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}
+  note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}}
 
 @manual{isabelle-jedit,
   author = {Makarius Wenzel},
   title = {{Isabelle/jEdit}},
-  note = {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}}
+  note = {\url{https://isabelle.in.tum.de/doc/jedit.pdf}}}
 
 @manual{isabelle-isar-ref,
   author = {Makarius Wenzel},
   title = {The {Isabelle/Isar} Reference Manual},
-  note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
+  note = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}
 
 @manual{isabelle-implementation,
   author = {Makarius Wenzel},
   title = {The {Isabelle/Isar} Implementation},
-  note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+  note = {\url{https://isabelle.in.tum.de/doc/implementation.pdf}}}
 
 @InProceedings{Wenzel:1999:TPHOL,
   author = 	 {Markus Wenzel},
diff -r 371e814af6f0 -r f849fc1cb65e src/HOL/Lattice/document/root.bib
--- a/src/HOL/Lattice/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/Lattice/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
@@ -27,7 +27,7 @@
   title         = {Using Axiomatic Type Classes in Isabelle},
   year          = 2000,
   institution   = {TU Munich},
-  note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/axclass.pdf}}
 }
 
 @Manual{Wenzel:2000:isar-ref,
@@ -35,7 +35,7 @@
   title         = {The {Isabelle/Isar} Reference Manual},
   year          = 2000,
   institution   = {TU Munich},
-  note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}
 }
 
 @Proceedings{tphols99,
diff -r 371e814af6f0 -r f849fc1cb65e src/HOL/MicroJava/document/introduction.tex
--- a/src/HOL/MicroJava/document/introduction.tex	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/MicroJava/document/introduction.tex	Wed Jul 18 16:44:01 2018 +0200
@@ -46,7 +46,7 @@
 
 For a more complete Isabelle model of JavaCard, the reader should
 consult the Bali formalization
-(\url{http://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
+(\url{https://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
 models most of the source language features of JavaCard, however without
 describing the bytecode level.
 
@@ -101,7 +101,7 @@
 Initialization during object creation is not accounted for in the
 present document 
 (see the formalization in
-\url{http://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
+\url{https://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
 neither is the \texttt{jsr} instruction.
 
 
diff -r 371e814af6f0 -r f849fc1cb65e src/HOL/MicroJava/document/root.bib
--- a/src/HOL/MicroJava/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/MicroJava/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
@@ -20,7 +20,7 @@
 embedding languages in theorem provers.},
         CRClassification = {D.3.1, F.3.2},
         CRGenTerms = {Languages, Reliability, Theory, Verification},
-        url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
+        url = {\url{https://isabelle.in.tum.de/Bali/papers/MOD99.html}},
         pages = {117--144}
 }
 
@@ -50,7 +50,7 @@
 theorem prover Isabelle/HOL.},
         CRClassification = {D.2.4, D.3.1, F.3.1},
         CRGenTerms = {Languages, Verification, Theory},
-        url       = {\url{http://isabelle.in.tum.de/Bali/papers/ECOOP00.html}}
+        url       = {\url{https://isabelle.in.tum.de/Bali/papers/ECOOP00.html}}
 }
 
 
diff -r 371e814af6f0 -r f849fc1cb65e src/HOL/NanoJava/document/root.bib
--- a/src/HOL/NanoJava/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/NanoJava/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
@@ -12,7 +12,7 @@
   and dynamic binding within method calls.},
         CRClassification = {D.3.1, F.3.2},
         CRGenTerms = {Languages, Reliability, Theory, Verification},
-        url = {\url{http://isabelle.in.tum.de/Bali/papers/NanoJava.html}},
+        url = {\url{https://isabelle.in.tum.de/Bali/papers/NanoJava.html}},
         note = {Submitted for publication.}
 }
 
@@ -38,7 +38,7 @@
 embedding languages in theorem provers.},
         CRClassification = {D.3.1, F.3.2},
         CRGenTerms = {Languages, Reliability, Theory, Verification},
-        url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
+        url = {\url{https://isabelle.in.tum.de/Bali/papers/MOD99.html}},
         pages = {117--144}
 }
 
@@ -74,5 +74,5 @@
 but also gives maximal confidence in the results obtained.},
         CRClassification = {D.2.4, D.3.1, F.3.1},
         CRGenTerms = {Languages, Verification, Theory},
-        note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}
+        note = {\url{https://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}
 }
diff -r 371e814af6f0 -r f849fc1cb65e src/HOL/NanoJava/document/root.tex
--- a/src/HOL/NanoJava/document/root.tex	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/NanoJava/document/root.tex	Wed Jul 18 16:44:01 2018 +0200
@@ -36,7 +36,7 @@
   implements a new approach for handling auxiliary variables.
   A more complex Hoare logic covering a much larger subset of Java is described
   in \cite{DvO-CPE01}.\\
-See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}
+See also the homepage of project Bali at \url{https://isabelle.in.tum.de/Bali/}
 and the conference version of this document \cite{NanoJava}.
 \end{abstract}
 
diff -r 371e814af6f0 -r f849fc1cb65e src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/ROOT	Wed Jul 18 16:44:01 2018 +0200
@@ -188,7 +188,7 @@
 
     This is an extension of IMP with local variables and mutually recursive
     procedures. For documentation see "Hoare Logic for Mutual Recursion and
-    Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
+    Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   *}
   theories EvenOdd
 
diff -r 371e814af6f0 -r f849fc1cb65e src/HOL/Unix/document/root.bib
--- a/src/HOL/Unix/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
+++ b/src/HOL/Unix/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
@@ -4,7 +4,7 @@
                   Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and
                   Markus Wenzel},
   title = 	 {The Supplemental {Isabelle/HOL} Library},
-  note = 	 {\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
+  note = 	 {\url{https://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
   year =	 2002
 }
 
@@ -21,7 +21,7 @@
   institution   = {Institut f\"ur Informatik, Technische Universi\"at
                   M\"unchen and Computer Laboratory, University of Cambridge},
   year          = 2000,
-  note          = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/logics-HOL.pdf}}
 }
 
 @Book{Tanenbaum:1992,
@@ -56,7 +56,7 @@
   title         = {The {Isabelle/Isar} Reference Manual},
   year          = 2002,
   institution   = {TU Munich},
-  note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
+  note          = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}
 }
 
 @Proceedings{tphols99,