--- 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}\@}
--- 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!)
--- 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}\@}
--- 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}}