doc-src/TutorialI/Rules/rules.tex

--- a/doc-src/TutorialI/Rules/rules.tex	Fri Jan 12 16:56:20 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jan 12 17:59:37 2001 +0100
@@ -922,7 +922,7 @@
 \end{exercise}
 
 
-\section{Hilbert's $\epsilon$-Operator}
+\section{Hilbert's Epsilon-Operator}
 
 Isabelle/HOL provides Hilbert's
 $\epsilon$-operator.  The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is