--- a/doc-src/TutorialI/Rules/rules.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Wed Jun 22 09:26:18 2005 +0200
@@ -635,10 +635,10 @@
filled in later, sometimes in stages and often automatically.
\begin{pgnote}
-If unification fails when you think it should succeed, try setting the Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
-\textsf{Trace Unification},
+If unification fails when you think it should succeed, try setting the Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
+\pgmenu{Trace Unification},
which makes Isabelle show the cause of unification failures (in Proof
-General's \textsf{Trace} buffer).
+General's \pgmenu{Trace} buffer).
\end{pgnote}
\noindent
For example, suppose we are trying to prove this subgoal by assumption: