doc-src/TutorialI/Rules/rules.tex
 changeset 10887 7fb42b97413a parent 10854 d1ff1ff5c5ad child 10967 69937e62a28e
equal inserted replaced
10886:f6b16554720d 10887:7fb42b97413a
   920 \emph{Hint}: the proof is similar
   920 \emph{Hint}: the proof is similar
   921 to the one just above for the universal quantifier.
   921 to the one just above for the universal quantifier.
   922 \end{exercise}
   922 \end{exercise}
   923
   923
   924
   924
   925 \section{Hilbert's $\epsilon$-Operator}
   925 \section{Hilbert's Epsilon-Operator}
   926
   926
   927 Isabelle/HOL provides Hilbert's
   927 Isabelle/HOL provides Hilbert's
   928 $\epsilon$-operator.  The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
   928 $\epsilon$-operator.  The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
   929 true, provided such a value exists.  Using this operator, we can express an
   929 true, provided such a value exists.  Using this operator, we can express an
   930 existential destruction rule:
   930 existential destruction rule: