diff -r c1e79e266fb3 -r b2d47981c8dc src/Doc/Tutorial/document/tutorial.sty --- a/src/Doc/Tutorial/document/tutorial.sty Wed May 19 15:45:13 2021 +0200 +++ b/src/Doc/Tutorial/document/tutorial.sty Wed May 19 15:53:55 2021 +0200 @@ -42,8 +42,6 @@ \newcommand\cmmdx[1]{\index{#1@\protect\isacommand{#1} (command)}} \newcommand\commdx[1]{\isacommand{#1}\index{#1@\protect\isacommand{#1} (command)}} \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!)