--- 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}