--- a/doc-src/TutorialI/Rules/rules.tex Tue Oct 20 13:20:42 2009 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Tue Oct 20 13:37:56 2009 +0200
@@ -1357,7 +1357,7 @@
some $x$ such that $P(x)$ is true, provided one exists.
Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.
-Here is the definition of~\cdx{inv}, which expresses inverses of
+Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_onto}, which we ignore here.} which expresses inverses of
functions:
\begin{isabelle}
inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%