diff -r 791a4655cae3 -r 764547b68538 doc-src/TutorialI/Rules/rules.tex
--- 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%