footnote: inv via inv_onto
authornipkow
Tue Oct 20 13:37:56 2009 +0200 (2009-10-20)
changeset 33015575bd6548df9
parent 33014 85d7a096e63f
child 33018 49abb2ae1379
child 33019 bcf56a64ce1a
child 33037 b22e44496dc2
footnote: inv via inv_onto
doc-src/TutorialI/Rules/rules.tex
     1.1 --- a/doc-src/TutorialI/Rules/rules.tex	Tue Oct 20 13:20:42 2009 +0200
     1.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Tue Oct 20 13:37:56 2009 +0200
     1.3 @@ -1357,7 +1357,7 @@
     1.4  some $x$ such that $P(x)$ is true, provided one exists.
     1.5  Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.
     1.6  
     1.7 -Here is the definition of~\cdx{inv}, which expresses inverses of
     1.8 +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
     1.9  functions:
    1.10  \begin{isabelle}
    1.11  inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%