--- a/doc-src/TutorialI/Rules/rules.tex Wed Oct 21 17:34:35 2009 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Oct 22 09:27:48 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},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_onto}, which we ignore here.} which expresses inverses of
+Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_into}, which we ignore here.} which expresses inverses of
functions:
\begin{isabelle}
inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%