--- 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.