# HG changeset patch
# User paulson
# Date 979318777 -3600
# Node ID 7fb42b97413a6fa7b4bf1d50817b247d6638ddc0
# Parent  f6b16554720d456d9678924d46bc3683c7056c3e
the \\epsilon character causes font errors in a section title

diff -r f6b16554720d -r 7fb42b97413a 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