diff -r f718767efd49 -r f8a734dc0fbc doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Wed Jun 22 09:26:18 2005 +0200
@@ -344,8 +344,8 @@
 Type \isa{real} is only available in the logic HOL-Complex, which is
 HOL extended with a definitional development of the real and complex
 numbers.  Base your theory upon theory \thydx{Complex_Main}, not the
-usual \isa{Main}, and set the Proof General menu item \textsf{Isabelle} $>$
-\textsf{Logics} $>$ \textsf{HOL-Complex}.%
+usual \isa{Main}, and set the Proof General menu item \pgmenu{Isabelle} $>$
+\pgmenu{Logics} $>$ \pgmenu{HOL-Complex}.%
 \index{real numbers|)}\index{*real (type)|)}
 \end{warn}
 
@@ -400,8 +400,8 @@
 Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right}
 express the same properties, only for fields.
 \begin{pgnote}
-Setting the flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
-\textsf{Show Sorts} will display the type classes of all type variables.
+Setting the flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
+\pgmenu{Show Sorts} will display the type classes of all type variables.
 \end{pgnote}
 \noindent
 Here is how the theorem \isa{field_mult_cancel_right} appears with the flag set.