src/HOL/MicroJava/document/introduction.tex
changeset 68649 f849fc1cb65e
parent 12914 71015f46b3c1
     1.1 --- a/src/HOL/MicroJava/document/introduction.tex	Wed Jul 18 12:21:55 2018 +0200
     1.2 +++ b/src/HOL/MicroJava/document/introduction.tex	Wed Jul 18 16:44:01 2018 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  
     1.5  For a more complete Isabelle model of JavaCard, the reader should
     1.6  consult the Bali formalization
     1.7 -(\url{http://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
     1.8 +(\url{https://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
     1.9  models most of the source language features of JavaCard, however without
    1.10  describing the bytecode level.
    1.11  
    1.12 @@ -101,7 +101,7 @@
    1.13  Initialization during object creation is not accounted for in the
    1.14  present document 
    1.15  (see the formalization in
    1.16 -\url{http://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
    1.17 +\url{https://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
    1.18  neither is the \texttt{jsr} instruction.
    1.19  
    1.20