summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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} |