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