Spell out anonymous function notation

thesis.tex

@@ -2325,7 +2325,10 @@ synonymous.
 
 For a function $f : A \to B$ (or partial function $f : A \pto B$) we
 write $f(a) = b$ to mean $(a, b) \in f$, and say that $f$ applied to
-$a$ returns $b$. The notation $f(a)$ means the application of $f$ to
+$a$ returns $b$. We write $f(P) \defas M$ for the definition of a
+function with pattern $P$ and expression $M$, and sometimes we will
+use the anonymous notation $P \mapsto M$ to mean $f(P) \defas M$ for
+some fresh $f$.  The notation $f(a)$ means the application of $f$ to
 $a$, and we say that $f(a)$ is defined whenever $f(a) = b$ for some
 $b$.
 %