src/HOL/MicroJava/document/introduction.tex
changeset 68649 f849fc1cb65e
parent 12914 71015f46b3c1
--- 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.