doc-src/TutorialI/Rules/rules.tex
changeset 11300 5b6887aedc76
parent 11255 ca546b170471
child 11406 2b17622e1929
equal deleted 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}