# HG changeset patch
# User nipkow
# Date 1256038676 -7200
# Node ID 575bd6548df9d86244c1d9a2252ef22b8c31cb93
# Parent  85d7a096e63f44aa81173e592ebd9dc935d6b4a0
footnote: inv via inv_onto

diff -r 85d7a096e63f -r 575bd6548df9 doc-src/TutorialI/Rules/rules.tex
--- 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%