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