
diff -r f718767efd49 -r f8a734dc0fbc doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/basics.tex	Wed Jun 22 09:26:18 2005 +0200
@@ -142,8 +142,8 @@
   and keeps quiet about it. Occasionally this may lead to
   misunderstandings between you and the system. If anything strange
   happens, we recommend that you ask Isabelle to display all type
-  information via the Proof General menu item \textsf{Isabelle} $>$
-  \textsf{Settings} $>$ \textsf{Show Types} (see \S\ref{sec:interface}
+  information via the Proof General menu item \pgmenu{Isabelle} $>$
+  \pgmenu{Settings} $>$ \pgmenu{Show Types} (see \S\ref{sec:interface}
   for details).
 \end{warn}%
 \index{types|)}
@@ -264,8 +264,8 @@
 Isabelle echoes your input, you can see which parentheses are dropped
 --- they were superfluous. If you are unsure how to interpret
 Isabelle's output because you don't know where the (dropped)
-parentheses go, set the Proof General flag \textsf{Isabelle} $>$
-\textsf{Settings} $>$ \textsf{Show Brackets} (see \S\ref{sec:interface}).
+parentheses go, set the Proof General flag \pgmenu{Isabelle} $>$
+\pgmenu{Settings} $>$ \pgmenu{Show Brackets} (see \S\ref{sec:interface}).
 \end{warn}
 
 
@@ -309,7 +309,7 @@
 should be avoided. Most of the tutorial is independent of the
 interface and is phrased in a neutral language. For example, the
 phrase ``to abandon a proof'' corresponds to the obvious
-action of clicking on the \textsf{Undo} symbol in Proof General.
+action of clicking on the \pgmenu{Undo} symbol in Proof General.
 Proof General specific information is often displayed in paragraphs
 identified by a miniature Proof General icon. Here are two examples:
 \begin{pgnote}
@@ -320,15 +320,15 @@
 in the appendix.
 
 Note that by default x-symbols are not enabled. You have to switch
-them on via the menu item \textsf{Proof-General} $>$ \textsf{Options} $>$
-\textsf{X-Symbols} (and save the option via the top-level
-\textsf{Options} menu).
+them on via the menu item \pgmenu{Proof-General} $>$ \pgmenu{Options} $>$
+\pgmenu{X-Symbols} (and save the option via the top-level
+\pgmenu{Options} menu).
 \end{pgnote}
 
 \begin{pgnote}
-Proof General offers the \textsf{Isabelle} menu for displaying
+Proof General offers the \pgmenu{Isabelle} menu for displaying
 information and setting flags. A particularly useful flag is
-\textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Show Types} which
+\pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgdx{Show Types} which
 causes Isabelle to output the type information that is usually
 suppressed. This is indispensible in case of errors of all kinds
 because often the types reveal the source of the problem. Once you
@@ -345,10 +345,7 @@
 for more details.}.
 
 \begin{pgnote}
-You can choose a different logic via the \textsf{Isabelle} $>$
-\textsf{Logics} menu. For example, you may want to work in the real
+You can choose a different logic via the \pgmenu{Isabelle} $>$
+\pgmenu{Logics} menu. For example, you may want to work in the real
 numbers, an extension of HOL (see \S\ref{sec:real}).
-% This is just excess baggage:
-%(You have to restart Proof General if you only compile the new logic
-%after having launching Proof General already).
 \end{pgnote}




