1.1 --- a/doc-src/TutorialI/tutorial.sty	Wed Jun 22 07:54:13 2005 +0200
     1.2 +++ b/doc-src/TutorialI/tutorial.sty	Wed Jun 22 09:26:18 2005 +0200
     1.3 @@ -44,6 +44,7 @@
     1.4  \newcommand\methdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (method)}}
     1.5  \newcommand\tooldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (tool)}}
     1.6  \newcommand\settdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (setting)}}
     1.7 +\newcommand\pgdx[1]{\pgmenu{#1}\index{#1@\protect\pgmenu{#1} (Proof General)}}
     1.8  
     1.9  %set argument in \bf font and index in ROMAN font (for definitions in text!)
    1.10  \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
    1.11 @@ -123,7 +124,7 @@
    1.12           \small \noindent \hangindent\parindent \hangafter=-2 
    1.13           \hbox to0pt{\hskip-\hangindent \pghead\hfill}\ignorespaces}%
    1.14    {\par\endgroup\medbreak}
    1.15 -
    1.16 +\newcommand{\pgmenu}[1]{\textsf{#1}}
    1.17  
    1.18  
    1.19  %%%% Standard logical symbols