prefer HTTPS;
authorwenzelm
Wed Jul 18 16:44:01 2018 +0200 (13 months ago ago)
changeset 68650f849fc1cb65e
parent 68648 371e814af6f0
child 68651 7538b5f301ea
prefer HTTPS;
Admin/components/README
README
src/Doc/How_to_Prove_it/document/root.bib
src/Doc/Locales/document/root.bib
src/Doc/Logics/document/preface.tex
src/Doc/Prog_Prove/document/intro-isabelle.tex
src/Doc/Prog_Prove/document/root.bib
src/Doc/Sledgehammer/document/root.tex
src/Doc/Sugar/document/root.bib
src/Doc/Tutorial/document/basics.tex
src/Doc/Tutorial/document/fp.tex
src/Doc/Tutorial/document/preface.tex
src/Doc/manual.bib
src/HOL/Lattice/document/root.bib
src/HOL/MicroJava/document/introduction.tex
src/HOL/MicroJava/document/root.bib
src/HOL/NanoJava/document/root.bib
src/HOL/NanoJava/document/root.tex
src/HOL/ROOT
src/HOL/Unix/document/root.bib
     1.1 --- a/Admin/components/README	Wed Jul 18 12:21:55 2018 +0200
     1.2 +++ b/Admin/components/README	Wed Jul 18 16:44:01 2018 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5  Isabelle components are managed as authentic .tar.gz archives in
     1.6  /home/isabelle/components from where they are made publicly available
     1.7 -on http://isabelle.in.tum.de/components/.
     1.8 +on https://isabelle.in.tum.de/components/.
     1.9  
    1.10  Visibility on the HTTP server depends on local Unix file permission:
    1.11  nonfree components should omit "read" mode for the Unix group/other;
     2.1 --- a/README	Wed Jul 18 12:21:55 2018 +0200
     2.2 +++ b/README	Wed Jul 18 16:44:01 2018 +0200
     2.3 @@ -34,10 +34,10 @@
     2.4     The Isabelle home page may be accessed from the following mirror
     2.5     sites:
     2.6  
     2.7 -     * http://www.cl.cam.ac.uk/research/hvg/Isabelle
     2.8 -     * http://isabelle.in.tum.de
     2.9 +     * https://www.cl.cam.ac.uk/research/hvg/Isabelle
    2.10 +     * https://isabelle.in.tum.de
    2.11       * http://mirror.cse.unsw.edu.au/pub/isabelle
    2.12 -     * http://mirror.clarkson.edu/isabelle
    2.13 +     * https://mirror.clarkson.edu/isabelle
    2.14  
    2.15    Mailing list
    2.16  
     3.1 --- a/src/Doc/How_to_Prove_it/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
     3.2 +++ b/src/Doc/How_to_Prove_it/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
     3.3 @@ -3,12 +3,12 @@
     3.4  @string{Springer="Springer-Verlag"}
     3.5  
     3.6  @manual{Main,author={Tobias Nipkow},title={What's in Main},
     3.7 -note={\url{http://isabelle.in.tum.de/doc/main.pdf}}}
     3.8 +note={\url{https://isabelle.in.tum.de/doc/main.pdf}}}
     3.9  
    3.10  @manual{ProgProve,author={Tobias Nipkow},
    3.11  title={Programming and Proving in Isabelle/HOL},
    3.12 -note={\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}}
    3.13 +note={\url{https://isabelle.in.tum.de/doc/prog-prove.pdf}}}
    3.14  
    3.15  @manual{IsarRef,author={Makarius Wenzel},
    3.16  title={The Isabelle/Isar Reference Manual},
    3.17 -note={\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
    3.18 +note={\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}
     4.1 --- a/src/Doc/Locales/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
     4.2 +++ b/src/Doc/Locales/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  @unpublished{IsarRef,
     4.5    author = "Markus Wenzel",
     4.6    title = "The {Isabelle/Isar} Reference Manual",
     4.7 -  note = "Part of the Isabelle distribution, \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}."
     4.8 +  note = "Part of the Isabelle distribution, \url{https://isabelle.in.tum.de/doc/isar-ref.pdf}."
     4.9  }
    4.10  
    4.11  @book {Jacobson1985,
     5.1 --- a/src/Doc/Logics/document/preface.tex	Wed Jul 18 12:21:55 2018 +0200
     5.2 +++ b/src/Doc/Logics/document/preface.tex	Wed Jul 18 16:44:01 2018 +0200
     5.3 @@ -56,7 +56,7 @@
     5.4  \begin{center}\small
     5.5    \begin{tabular}{l}
     5.6      \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
     5.7 -    \url{http://isabelle.in.tum.de/library/} \\
     5.8 +    \url{https://isabelle.in.tum.de/library/} \\
     5.9    \end{tabular}
    5.10  \end{center}
    5.11  
     6.1 --- a/src/Doc/Prog_Prove/document/intro-isabelle.tex	Wed Jul 18 12:21:55 2018 +0200
     6.2 +++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex	Wed Jul 18 16:44:01 2018 +0200
     6.3 @@ -56,7 +56,7 @@
     6.4  
     6.5  If you have not done so already, download and install Isabelle
     6.6  (this book is compatible with Isabelle2016-1)
     6.7 -from \url{http://isabelle.in.tum.de}. You can start it by clicking
     6.8 +from \url{https://isabelle.in.tum.de}. You can start it by clicking
     6.9  on the application icon. This will launch Isabelle's
    6.10  user interface based on the text editor \concept{jEdit}. Below you see
    6.11  a typical example snapshot of a session. At this point we merely explain
     7.1 --- a/src/Doc/Prog_Prove/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
     7.2 +++ b/src/Doc/Prog_Prove/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
     7.3 @@ -13,10 +13,10 @@
     7.4  
     7.5  @manual{Krauss,author={Alexander Krauss},
     7.6  title={Defining Recursive Functions in Isabelle/HOL},
     7.7 -note={\url{http://isabelle.in.tum.de/doc/functions.pdf}}}
     7.8 +note={\url{https://isabelle.in.tum.de/doc/functions.pdf}}}
     7.9  
    7.10  @manual{Nipkow-Main,author={Tobias Nipkow},title={What's in Main},
    7.11 -note={\url{http://isabelle.in.tum.de/doc/main.pdf}}}
    7.12 +note={\url{https://isabelle.in.tum.de/doc/main.pdf}}}
    7.13  
    7.14  @book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
    7.15  title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
    7.16 @@ -28,4 +28,4 @@
    7.17  
    7.18  @manual{IsarRef,author={Makarius Wenzel},
    7.19  title={The Isabelle/Isar Reference Manual},
    7.20 -note={\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
    7.21 +note={\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}
     8.1 --- a/src/Doc/Sledgehammer/document/root.tex	Wed Jul 18 12:21:55 2018 +0200
     8.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jul 18 16:44:01 2018 +0200
     8.3 @@ -13,7 +13,7 @@
     8.4  %\usepackage[scaled=.85]{beramono}
     8.5  \usepackage{isabelle,iman,pdfsetup}
     8.6  
     8.7 -\newcommand\download{\url{http://isabelle.in.tum.de/components/}}
     8.8 +\newcommand\download{\url{https://isabelle.in.tum.de/components/}}
     8.9  
    8.10  \let\oldS=\S
    8.11  \def\S{\oldS\,}
     9.1 --- a/src/Doc/Sugar/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
     9.2 +++ b/src/Doc/Sugar/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
     9.3 @@ -8,5 +8,5 @@
     9.4  
     9.5  @misc{tar,author={Gerwin Klein and Norber Schirmer and Tobias Nipkow},
     9.6  title={{LaTeX} sugar theories and support files}, 
     9.7 -note={\url{http://isabelle.in.tum.de/sugar.tar.gz}}}
     9.8 +note={\url{https://isabelle.in.tum.de/sugar.tar.gz}}}
     9.9  
    10.1 --- a/src/Doc/Tutorial/document/basics.tex	Wed Jul 18 12:21:55 2018 +0200
    10.2 +++ b/src/Doc/Tutorial/document/basics.tex	Wed Jul 18 16:44:01 2018 +0200
    10.3 @@ -85,7 +85,7 @@
    10.4  \end{warn}
    10.5  HOL's theory collection is available online at
    10.6  \begin{center}\small
    10.7 -    \url{http://isabelle.in.tum.de/library/HOL/}
    10.8 +    \url{https://isabelle.in.tum.de/library/HOL/}
    10.9  \end{center}
   10.10  and is recommended browsing. In subdirectory \texttt{Library} you find
   10.11  a growing library of useful theories that are not part of \isa{Main}
    11.1 --- a/src/Doc/Tutorial/document/fp.tex	Wed Jul 18 12:21:55 2018 +0200
    11.2 +++ b/src/Doc/Tutorial/document/fp.tex	Wed Jul 18 16:44:01 2018 +0200
    11.3 @@ -130,7 +130,7 @@
    11.4  Lists are one of the essential datatypes in computing.  We expect that you
    11.5  are already familiar with their basic operations.
    11.6  Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
    11.7 -\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
    11.8 +\thydx{List}\footnote{\url{https://isabelle.in.tum.de/library/HOL/List.html}}.
    11.9  The latter contains many further operations. For example, the functions
   11.10  \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
   11.11  element and the remainder of a list. (However, pattern matching is usually
    12.1 --- a/src/Doc/Tutorial/document/preface.tex	Wed Jul 18 12:21:55 2018 +0200
    12.2 +++ b/src/Doc/Tutorial/document/preface.tex	Wed Jul 18 16:44:01 2018 +0200
    12.3 @@ -35,7 +35,7 @@
    12.4  from output generated in this way.  The final chapter of Part~I explains how
    12.5  users may produce their own formal documents in a similar fashion.
    12.6  
    12.7 -Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains
    12.8 +Isabelle's \hfootref{https://isabelle.in.tum.de/}{web site} contains
    12.9  links to the download area and to documentation and other information.
   12.10  The classic Isabelle user interface is Proof~General~/ Emacs by David
   12.11  Aspinall's\index{Aspinall, David}.  This book says very little about
    13.1 --- a/src/Doc/manual.bib	Wed Jul 18 12:21:55 2018 +0200
    13.2 +++ b/src/Doc/manual.bib	Wed Jul 18 16:44:01 2018 +0200
    13.3 @@ -158,7 +158,7 @@
    13.4    author        = {Clemens Ballarin},
    13.5    title         = {Tutorial to Locales and Locale Interpretation},
    13.6    institution   = TUM,
    13.7 -  note          = {\url{http://isabelle.in.tum.de/doc/locales.pdf}}
    13.8 +  note          = {\url{https://isabelle.in.tum.de/doc/locales.pdf}}
    13.9  }
   13.10  
   13.11  @article{Ballarin2014,
   13.12 @@ -226,7 +226,7 @@
   13.13                    Markus Wenzel},
   13.14    title =        {The Supplemental {Isabelle/HOL} Library},
   13.15    note =         {Part of the Isabelle distribution,
   13.16 -                  \url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
   13.17 +                  \url{https://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
   13.18    year =         2002
   13.19  }
   13.20  
   13.21 @@ -311,7 +311,7 @@
   13.22    author	= {Julian Biendarra and Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel},
   13.23    title		= {Defining (Co)datatypes and Primitively (Co)recursive Functions in {Isabelle\slash HOL}},
   13.24    institution	= {TU Munich},
   13.25 -  note          = {\url{http://isabelle.in.tum.de/doc/datatypes.pdf}}}
   13.26 +  note          = {\url{https://isabelle.in.tum.de/doc/datatypes.pdf}}}
   13.27  
   13.28  @book{Bird-Wadler,author="Richard Bird and Philip Wadler",
   13.29  title="Introduction to Functional Programming",publisher=PH,year=1988}
   13.30 @@ -324,21 +324,21 @@
   13.31    author        = {Jasmin Christian Blanchette},
   13.32    title         = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle\slash {HOL}},
   13.33    institution   = TUM,
   13.34 -  note          = {\url{http://isabelle.in.tum.de/doc/nitpick.pdf}}
   13.35 +  note          = {\url{https://isabelle.in.tum.de/doc/nitpick.pdf}}
   13.36  }
   13.37  
   13.38  @manual{isabelle-sledgehammer,
   13.39    author        = {Jasmin Christian Blanchette},
   13.40    title         = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle\slash {HOL}},
   13.41    institution   = TUM,
   13.42 -  note          = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}
   13.43 +  note          = {\url{https://isabelle.in.tum.de/doc/sledgehammer.pdf}}
   13.44  }
   13.45  
   13.46  @manual{isabelle-corec,
   13.47    author	= {Jasmin Christian Blanchette and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel},
   13.48    title		= {Defining Nonprimitively Corecursive Functions in {Isabelle\slash HOL}},
   13.49    institution	= {TU Munich},
   13.50 -  note          = {\url{http://isabelle.in.tum.de/doc/corec.pdf}}}
   13.51 +  note          = {\url{https://isabelle.in.tum.de/doc/corec.pdf}}}
   13.52  
   13.53  @inproceedings{blanchette-nipkow-2010,
   13.54    title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
   13.55 @@ -831,14 +831,14 @@
   13.56    author        = {Florian Haftmann},
   13.57    title         = {Haskell-style type classes with {Isabelle}/{Isar}},
   13.58    institution   = TUM,
   13.59 -  note          = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}
   13.60 +  note          = {\url{https://isabelle.in.tum.de/doc/classes.pdf}}
   13.61  }
   13.62  
   13.63  @manual{isabelle-codegen,
   13.64    author        = {Florian Haftmann},
   13.65    title         = {Code generation from Isabelle theories},
   13.66    institution   = TUM,
   13.67 -  note          = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}
   13.68 +  note          = {\url{https://isabelle.in.tum.de/doc/codegen.pdf}}
   13.69  }
   13.70  
   13.71  @Book{halmos60,
   13.72 @@ -1064,7 +1064,7 @@
   13.73    author        = {Alexander Krauss},
   13.74    title         = {Defining Recursive Functions in {Isabelle/HOL}},
   13.75    institution   = TUM,
   13.76 -  note          = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
   13.77 +  note          = {\url{https://isabelle.in.tum.de/doc/functions.pdf}}
   13.78  }
   13.79  
   13.80  @inproceedings{Kuncar:2015,
   13.81 @@ -1366,7 +1366,7 @@
   13.82    title		= {{Isabelle}'s Logics: {HOL}},
   13.83    institution	= {Institut f{\"u}r Informatik, Technische Universi{\"a}t
   13.84                    M{\"u}nchen and Computer Laboratory, University of Cambridge},
   13.85 -  note          = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
   13.86 +  note          = {\url{https://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
   13.87  
   13.88  @article{nipkow-prehofer,
   13.89    author	= {Tobias Nipkow and Christian Prehofer},
   13.90 @@ -1502,25 +1502,25 @@
   13.91    author	= {Lawrence C. Paulson},
   13.92    title		= {Old Introduction to {Isabelle}},
   13.93    institution	= CUCL,
   13.94 -  note          = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}}
   13.95 +  note          = {\url{https://isabelle.in.tum.de/doc/intro.pdf}}}
   13.96  
   13.97  @manual{isabelle-logics,
   13.98    author	= {Lawrence C. Paulson},
   13.99    title		= {{Isabelle's} Logics},
  13.100    institution	= CUCL,
  13.101 -  note          = {\url{http://isabelle.in.tum.de/doc/logics.pdf}}}
  13.102 +  note          = {\url{https://isabelle.in.tum.de/doc/logics.pdf}}}
  13.103  
  13.104  @manual{isabelle-ref,
  13.105    author	= {Lawrence C. Paulson},
  13.106    title		= {The Old {Isabelle} Reference Manual},
  13.107    institution	= CUCL,
  13.108 -  note          = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}}
  13.109 +  note          = {\url{https://isabelle.in.tum.de/doc/ref.pdf}}}
  13.110  
  13.111  @manual{isabelle-ZF,
  13.112    author	= {Lawrence C. Paulson},
  13.113    title		= {{Isabelle}'s Logics: {FOL} and {ZF}},
  13.114    institution	= CUCL,
  13.115 -  note          = {\url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}}}
  13.116 +  note          = {\url{https://isabelle.in.tum.de/doc/logics-ZF.pdf}}}
  13.117  
  13.118  @article{paulson-found,
  13.119    author	= {Lawrence C. Paulson},
  13.120 @@ -2024,22 +2024,22 @@
  13.121  @manual{isabelle-system,
  13.122    author = {Makarius Wenzel},
  13.123    title = {The {Isabelle} System Manual},
  13.124 -  note = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}
  13.125 +  note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}}
  13.126  
  13.127  @manual{isabelle-jedit,
  13.128    author = {Makarius Wenzel},
  13.129    title = {{Isabelle/jEdit}},
  13.130 -  note = {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}}
  13.131 +  note = {\url{https://isabelle.in.tum.de/doc/jedit.pdf}}}
  13.132  
  13.133  @manual{isabelle-isar-ref,
  13.134    author = {Makarius Wenzel},
  13.135    title = {The {Isabelle/Isar} Reference Manual},
  13.136 -  note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
  13.137 +  note = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}
  13.138  
  13.139  @manual{isabelle-implementation,
  13.140    author = {Makarius Wenzel},
  13.141    title = {The {Isabelle/Isar} Implementation},
  13.142 -  note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
  13.143 +  note = {\url{https://isabelle.in.tum.de/doc/implementation.pdf}}}
  13.144  
  13.145  @InProceedings{Wenzel:1999:TPHOL,
  13.146    author = 	 {Markus Wenzel},
    14.1 --- a/src/HOL/Lattice/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
    14.2 +++ b/src/HOL/Lattice/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
    14.3 @@ -27,7 +27,7 @@
    14.4    title         = {Using Axiomatic Type Classes in Isabelle},
    14.5    year          = 2000,
    14.6    institution   = {TU Munich},
    14.7 -  note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}
    14.8 +  note          = {\url{https://isabelle.in.tum.de/doc/axclass.pdf}}
    14.9  }
   14.10  
   14.11  @Manual{Wenzel:2000:isar-ref,
   14.12 @@ -35,7 +35,7 @@
   14.13    title         = {The {Isabelle/Isar} Reference Manual},
   14.14    year          = 2000,
   14.15    institution   = {TU Munich},
   14.16 -  note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
   14.17 +  note          = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}
   14.18  }
   14.19  
   14.20  @Proceedings{tphols99,
    15.1 --- a/src/HOL/MicroJava/document/introduction.tex	Wed Jul 18 12:21:55 2018 +0200
    15.2 +++ b/src/HOL/MicroJava/document/introduction.tex	Wed Jul 18 16:44:01 2018 +0200
    15.3 @@ -46,7 +46,7 @@
    15.4  
    15.5  For a more complete Isabelle model of JavaCard, the reader should
    15.6  consult the Bali formalization
    15.7 -(\url{http://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
    15.8 +(\url{https://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
    15.9  models most of the source language features of JavaCard, however without
   15.10  describing the bytecode level.
   15.11  
   15.12 @@ -101,7 +101,7 @@
   15.13  Initialization during object creation is not accounted for in the
   15.14  present document 
   15.15  (see the formalization in
   15.16 -\url{http://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
   15.17 +\url{https://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
   15.18  neither is the \texttt{jsr} instruction.
   15.19  
   15.20  
    16.1 --- a/src/HOL/MicroJava/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
    16.2 +++ b/src/HOL/MicroJava/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
    16.3 @@ -20,7 +20,7 @@
    16.4  embedding languages in theorem provers.},
    16.5          CRClassification = {D.3.1, F.3.2},
    16.6          CRGenTerms = {Languages, Reliability, Theory, Verification},
    16.7 -        url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
    16.8 +        url = {\url{https://isabelle.in.tum.de/Bali/papers/MOD99.html}},
    16.9          pages = {117--144}
   16.10  }
   16.11  
   16.12 @@ -50,7 +50,7 @@
   16.13  theorem prover Isabelle/HOL.},
   16.14          CRClassification = {D.2.4, D.3.1, F.3.1},
   16.15          CRGenTerms = {Languages, Verification, Theory},
   16.16 -        url       = {\url{http://isabelle.in.tum.de/Bali/papers/ECOOP00.html}}
   16.17 +        url       = {\url{https://isabelle.in.tum.de/Bali/papers/ECOOP00.html}}
   16.18  }
   16.19  
   16.20  
    17.1 --- a/src/HOL/NanoJava/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
    17.2 +++ b/src/HOL/NanoJava/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
    17.3 @@ -12,7 +12,7 @@
    17.4    and dynamic binding within method calls.},
    17.5          CRClassification = {D.3.1, F.3.2},
    17.6          CRGenTerms = {Languages, Reliability, Theory, Verification},
    17.7 -        url = {\url{http://isabelle.in.tum.de/Bali/papers/NanoJava.html}},
    17.8 +        url = {\url{https://isabelle.in.tum.de/Bali/papers/NanoJava.html}},
    17.9          note = {Submitted for publication.}
   17.10  }
   17.11  
   17.12 @@ -38,7 +38,7 @@
   17.13  embedding languages in theorem provers.},
   17.14          CRClassification = {D.3.1, F.3.2},
   17.15          CRGenTerms = {Languages, Reliability, Theory, Verification},
   17.16 -        url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
   17.17 +        url = {\url{https://isabelle.in.tum.de/Bali/papers/MOD99.html}},
   17.18          pages = {117--144}
   17.19  }
   17.20  
   17.21 @@ -74,5 +74,5 @@
   17.22  but also gives maximal confidence in the results obtained.},
   17.23          CRClassification = {D.2.4, D.3.1, F.3.1},
   17.24          CRGenTerms = {Languages, Verification, Theory},
   17.25 -        note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}
   17.26 +        note = {\url{https://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}
   17.27  }
    18.1 --- a/src/HOL/NanoJava/document/root.tex	Wed Jul 18 12:21:55 2018 +0200
    18.2 +++ b/src/HOL/NanoJava/document/root.tex	Wed Jul 18 16:44:01 2018 +0200
    18.3 @@ -36,7 +36,7 @@
    18.4    implements a new approach for handling auxiliary variables.
    18.5    A more complex Hoare logic covering a much larger subset of Java is described
    18.6    in \cite{DvO-CPE01}.\\
    18.7 -See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}
    18.8 +See also the homepage of project Bali at \url{https://isabelle.in.tum.de/Bali/}
    18.9  and the conference version of this document \cite{NanoJava}.
   18.10  \end{abstract}
   18.11  
    19.1 --- a/src/HOL/ROOT	Wed Jul 18 12:21:55 2018 +0200
    19.2 +++ b/src/HOL/ROOT	Wed Jul 18 16:44:01 2018 +0200
    19.3 @@ -188,7 +188,7 @@
    19.4  
    19.5      This is an extension of IMP with local variables and mutually recursive
    19.6      procedures. For documentation see "Hoare Logic for Mutual Recursion and
    19.7 -    Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
    19.8 +    Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
    19.9    *}
   19.10    theories EvenOdd
   19.11  
    20.1 --- a/src/HOL/Unix/document/root.bib	Wed Jul 18 12:21:55 2018 +0200
    20.2 +++ b/src/HOL/Unix/document/root.bib	Wed Jul 18 16:44:01 2018 +0200
    20.3 @@ -4,7 +4,7 @@
    20.4                    Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and
    20.5                    Markus Wenzel},
    20.6    title = 	 {The Supplemental {Isabelle/HOL} Library},
    20.7 -  note = 	 {\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
    20.8 +  note = 	 {\url{https://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
    20.9    year =	 2002
   20.10  }
   20.11  
   20.12 @@ -21,7 +21,7 @@
   20.13    institution   = {Institut f\"ur Informatik, Technische Universi\"at
   20.14                    M\"unchen and Computer Laboratory, University of Cambridge},
   20.15    year          = 2000,
   20.16 -  note          = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}
   20.17 +  note          = {\url{https://isabelle.in.tum.de/doc/logics-HOL.pdf}}
   20.18  }
   20.19  
   20.20  @Book{Tanenbaum:1992,
   20.21 @@ -56,7 +56,7 @@
   20.22    title         = {The {Isabelle/Isar} Reference Manual},
   20.23    year          = 2002,
   20.24    institution   = {TU Munich},
   20.25 -  note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
   20.26 +  note          = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}
   20.27  }
   20.28  
   20.29  @Proceedings{tphols99,