doc-src/Tutorial/fp.tex

 case study.
 
 
 \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}
 \label{sec:general-datatype}