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}