--- a/doc-src/Tutorial/fp.tex Mon May 10 17:07:19 1999 +0200
+++ b/doc-src/Tutorial/fp.tex Mon May 10 17:43:55 1999 +0200
@@ -358,7 +358,7 @@
Lists are one of the essential datatypes in computing. Readers of this
tutorial and users of HOL need to be familiar with their basic operations.
Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory
-\texttt{List}\footnote{\texttt{http://isabelle.in.tum.de/library/HOL/List.html}}.
+\texttt{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
The latter contains many further operations. For example, the functions
\ttindexbold{hd} (`head') and \ttindexbold{tl} (`tail') return the first
element and the remainder of a list. (However, pattern-matching is usually