doc-src/TutorialI/Rules/rules.tex
 changeset 11300 5b6887aedc76 parent 11255 ca546b170471 child 11406 2b17622e1929
equal inserted replaced
11299:1d3d110c456e 11300:5b6887aedc76
1384 The original purpose of Hilbert's $\varepsilon$-operator was to express an
1384 The original purpose of Hilbert's $\varepsilon$-operator was to express an
1385 existential destruction rule:
1385 existential destruction rule:
1386 $\infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P}$
1386 $\infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P}$
1387 This rule is seldom used for that purpose --- it can cause exponential
1387 This rule is seldom used for that purpose --- it can cause exponential
1388 blow-up --- but it is occasionally used as an introduction rule
1388 blow-up --- but it is occasionally used as an introduction rule
1389 for~$\varepsilon$-operator.  Its name is HOL is \isa{someI_ex}.
1389 for~$\varepsilon$-operator.  Its name in HOL is \isa{someI_ex}.
1390
1390
1391
1391
1392 \index{Hilbert's epsilon-operator|)}
1392 \index{Hilbert's epsilon-operator|)}
1393
1393
1394 \section{Some Proofs That Fail}
1394 \section{Some Proofs That Fail}