# HG changeset patch
# User wenzelm
# Date 1621432435 -7200
# Node ID b2d47981c8dc751f9ad53e0369183ec1c7c56282
# Parent  c1e79e266fb31715e1b5e07b09be888575798975
unused;

diff -r c1e79e266fb3 -r b2d47981c8dc src/Doc/Logics_ZF/document/logics.sty
--- a/src/Doc/Logics_ZF/document/logics.sty	Wed May 19 15:45:13 2021 +0200
+++ b/src/Doc/Logics_ZF/document/logics.sty	Wed May 19 15:53:55 2021 +0200
@@ -40,8 +40,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)}}
 
 %set argument in \bf font and index in ROMAN font (for definitions in text!)
 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
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!)
diff -r c1e79e266fb3 -r b2d47981c8dc src/Doc/iman.sty
--- a/src/Doc/iman.sty	Wed May 19 15:45:13 2021 +0200
+++ b/src/Doc/iman.sty	Wed May 19 15:53:55 2021 +0200
@@ -31,16 +31,10 @@
 \newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
 \newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
 
-\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
-\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
-
 \newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
 \newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} type}}
 \newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
 
-\newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}
-\newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}
-
 %set argument in \tt font; at the same time, index using * prefix
 \newcommand\rmindex[1]{{#1}\index{#1}\@}
 \newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
diff -r c1e79e266fb3 -r b2d47981c8dc src/Doc/isar.sty
--- a/src/Doc/isar.sty	Wed May 19 15:45:13 2021 +0200
+++ b/src/Doc/isar.sty	Wed May 19 15:53:55 2021 +0200
@@ -9,8 +9,6 @@
 \newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt #1}}
 \newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt isabelle #1}}
 
-\newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}}
-\newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
 \newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
 
 \newcommand{\isasymIF}{\isakeyword{if}}