diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Tue Jul 17 13:46:21 2001 +0200
@@ -57,7 +57,7 @@
 proofs seen so far could have been performed
 with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
 only the first subgoal and may thus need to be repeated --- use
-\isaindex{simp_all} to simplify all subgoals.
+\methdx{simp_all} to simplify all subgoals.
 Note that \isa{simp} fails if nothing changes.%
 \end{isamarkuptext}%
 %
@@ -138,7 +138,7 @@
 Assumptions are simplified in a left-to-right fashion. If an
 assumption can help in simplifying one to the left of it, this may get
 overlooked. In such cases you have to rotate the assumptions explicitly:
-\isacommand{apply}\isa{{\isacharparenleft}rotate{\isacharunderscore}tac}~$n$\isa{{\isacharparenright}}\indexbold{*rotate_tac}
+\isacommand{apply}\isa{{\isacharparenleft}}\methdx{rotate_tac}~$n$\isa{{\isacharparenright}}
 causes a cyclic shift by $n$ positions from right to left, if $n$ is
 positive, and from left to right, if $n$ is negative.
 Beware that such rotations make proofs quite brittle.
@@ -167,8 +167,8 @@
 \isacommand{lemma}\ {\isachardoublequote}xor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
-Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
-get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
+Typically, we begin by unfolding some definitions:
+\indexbold{definitions!unfolding}%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptxt}%
@@ -200,7 +200,7 @@
 %
 \begin{isamarkuptext}%
 \index{simplification!of let-expressions}
-Proving a goal containing \isaindex{let}-expressions almost invariably
+Proving a goal containing \sdx{let}-expressions almost invariably
 requires the \isa{let}-con\-structs to be expanded at some point. Since
 \isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for a predefined constant
 (called \isa{Let}), expanding \isa{let}-constructs means rewriting with
@@ -262,13 +262,13 @@
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isasymforall}xs{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}%
 \end{isabelle}
-where \isaindexbold{split_if} is a theorem that expresses splitting of
+where \tdx{split_if} is a theorem that expresses splitting of
 \isa{if}s. Because
 case-splitting on \isa{if}s is almost always the right proof strategy, the
 simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
 on the initial goal above.
 
-This splitting idea generalizes from \isa{if} to \isaindex{case}.
+This splitting idea generalizes from \isa{if} to \sdx{case}.
 Let us simplify a case analysis over lists:%
 \end{isamarkuptxt}%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
@@ -334,7 +334,7 @@
   The simplifier merely simplifies the condition of an \isa{if} but not the
   \isa{then} or \isa{else} parts. The latter are simplified only after the
   condition reduces to \isa{True} or \isa{False}, or after splitting. The
-  same is true for \isaindex{case}-expressions: only the selector is
+  same is true for \sdx{case}-expressions: only the selector is
   simplified at first, until either the expression reduces to one of the
   cases or it is split.
 \end{warn}\index{*split (method, attr.)|)}%
@@ -344,7 +344,7 @@
 }
 %
 \begin{isamarkuptext}%
-\index{arithmetic}
+\index{linear arithmetic}
 The simplifier routinely solves a small class of linear arithmetic formulae
 (over type \isa{nat} and other numeric types): it only takes into account
 assumptions and conclusions that are relations
@@ -367,7 +367,8 @@
 \begin{isamarkuptext}%
 \indexbold{tracing the simplifier}
 Using the simplifier effectively may take a bit of experimentation.  Set the
-\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
+\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} 
+to get a better idea of what is going
 on:%
 \end{isamarkuptext}%
 \isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline