doc-src/TutorialI/Rules/rules.tex

 \bigisa{?z2} to the identity function.
 
 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 
 may need to search among different ways of proving certain 
 subgoals. Often a choice that proves one subgoal renders another