src/Doc/Tutorial/document/fp.tex
changeset 68649 f849fc1cb65e
parent 57083 5c26000e1042
     1.1 --- a/src/Doc/Tutorial/document/fp.tex	Wed Jul 18 12:21:55 2018 +0200
     1.2 +++ b/src/Doc/Tutorial/document/fp.tex	Wed Jul 18 16:44:01 2018 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4  Lists are one of the essential datatypes in computing.  We expect that you
     1.5  are already familiar with their basic operations.
     1.6  Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
     1.7 -\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
     1.8 +\thydx{List}\footnote{\url{https://isabelle.in.tum.de/library/HOL/List.html}}.
     1.9  The latter contains many further operations. For example, the functions
    1.10  \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
    1.11  element and the remainder of a list. (However, pattern matching is usually