--- 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;
--- 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
--- 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}}}
--- 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,
--- 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}
--- 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
--- 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}}}
--- 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\,}
--- 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}}}
--- 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}
--- 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
--- 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
--- 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},
--- 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,
--- 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.
--- 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}}
}
--- 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}
}
--- 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}
--- 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
--- 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,