doc-src/TutorialI/Rules/rules.tex
changeset 10887 7fb42b97413a
parent 10854 d1ff1ff5c5ad
child 10967 69937e62a28e
equal deleted 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: