--- a/doc-src/TutorialI/fp.tex Fri Nov 02 12:35:27 2007 +0100
+++ b/doc-src/TutorialI/fp.tex Fri Nov 02 15:56:49 2007 +0100
@@ -133,7 +133,7 @@
\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
The latter contains many further operations. For example, the functions
\cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
-element and the remainder of a list. (However, pattern-matching is usually
+element and the remainder of a list. (However, pattern matching is usually
preferable to \isa{hd} and \isa{tl}.)
Also available are higher-order functions like \isa{map} and \isa{filter}.
Theory \isa{List} also contains
@@ -465,7 +465,7 @@
Although many total functions have a natural primitive recursive definition,
this is not always the case. Arbitrary total recursive functions can be
-defined by means of \isacommand{fun}: you can use full pattern-matching,
+defined by means of \isacommand{fun}: you can use full pattern matching,
recursion need not involve datatypes, and termination is proved by showing
that the arguments of all recursive calls are smaller in a suitable sense.
In this section we restrict ourselves to functions where Isabelle can prove