--- a/doc-src/Tutorial/fp.tex Wed Jan 20 17:59:19 1999 +0100
+++ b/doc-src/Tutorial/fp.tex Wed Jan 20 18:07:34 1999 +0100
@@ -355,19 +355,18 @@
\subsection{Lists}
-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://www.in.tum.de/\~\relax
- isabelle/library/HOL/List.html}}.
+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}}.
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
-preferable to \texttt{hd} and \texttt{tl}.)
-Theory \texttt{List} also contains more syntactic sugar:
+preferable to \texttt{hd} and \texttt{tl}.) Theory \texttt{List} also
+contains more syntactic sugar:
\texttt{[}$x@1$\texttt{,}\dots\texttt{,}$x@n$\texttt{]} abbreviates
-$x@1$\texttt{\#}\dots\texttt{\#}$x@n$\texttt{\#[]}.
-In the rest of the tutorial we always use HOL's predefined lists.
+$x@1$\texttt{\#}\dots\texttt{\#}$x@n$\texttt{\#[]}. In the rest of the
+tutorial we always use HOL's predefined lists.
\subsection{The general format}