--- a/doc-src/TutorialI/Rules/rules.tex Mon Dec 04 17:29:48 2000 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Mon Dec 04 17:30:15 2000 +0100
@@ -1026,7 +1026,7 @@
This example is typical of how Isabelle enforces sound quantifier reasoning.
-\section{Proving theorems using the \emph{\texttt{blast}} method}
+\section{Proving theorems using the {\tt\slshape blast} method}
It is hard to prove substantial theorems using the methods
described above. A proof may be dozens or hundreds of steps long. You