# HG changeset patch # User paulson # Date 990028728 -7200 # Node ID 5b6887aedc7676e1adc24f8f96ba7e91ac0b364f # Parent 1d3d110c456e124cdc161b22f2d6b3b9de6bdc6d typo diff -r 1d3d110c456e -r 5b6887aedc76 doc-src/TutorialI/Rules/rules.tex --- a/doc-src/TutorialI/Rules/rules.tex Wed May 16 12:31:25 2001 +0200 +++ b/doc-src/TutorialI/Rules/rules.tex Wed May 16 17:58:48 2001 +0200 @@ -1386,7 +1386,7 @@ \[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \] This rule is seldom used for that purpose --- it can cause exponential blow-up --- but it is occasionally used as an introduction rule -for~$\varepsilon$-operator. Its name is HOL is \isa{someI_ex}. +for~$\varepsilon$-operator. Its name in HOL is \isa{someI_ex}. \index{Hilbert's epsilon-operator|)}