doc-src/TutorialI/tutorial.sty
changeset 16523 f8a734dc0fbc
parent 16087 89d0ee1fb198
--- a/doc-src/TutorialI/tutorial.sty	Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/tutorial.sty	Wed Jun 22 09:26:18 2005 +0200
@@ -44,6 +44,7 @@
 \newcommand\methdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (method)}}
 \newcommand\tooldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (tool)}}
 \newcommand\settdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (setting)}}
+\newcommand\pgdx[1]{\pgmenu{#1}\index{#1@\protect\pgmenu{#1} (Proof General)}}
 
 %set argument in \bf font and index in ROMAN font (for definitions in text!)
 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
@@ -123,7 +124,7 @@
          \small \noindent \hangindent\parindent \hangafter=-2 
          \hbox to0pt{\hskip-\hangindent \pghead\hfill}\ignorespaces}%
   {\par\endgroup\medbreak}
-
+\newcommand{\pgmenu}[1]{\textsf{#1}}
 
 
 %%%% Standard logical symbols