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




