diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Thu Jan 25 15:31:31 2001 +0100
@@ -234,8 +234,8 @@
 Recall that the conjunction elimination rules --- whose Isabelle names are 
 \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
 of a conjunction.  Rules of this sort (where the conclusion is a subformula of a
-premise) are called \textbf{destruction} rules, by analogy with the destructor
-functions of functional programming.%
+premise) are called \textbf{destruction} rules because they take apart and destroy
+a premise.%
 \footnote{This Isabelle terminology has no counterpart in standard logic texts, 
 although the distinction between the two forms of elimination rule is well known. 
 Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules 
@@ -365,7 +365,7 @@
 conclusion.  
 
 \medskip
-\indexbold{by}
+\indexbold{*by}
 The \isacommand{by} command is useful for proofs like these that use
 \isa{assumption} heavily.  It executes an
 \isacommand{apply} command, then tries to prove all remaining subgoals using
@@ -781,7 +781,7 @@
 To see how this works, let us derive a rule about reducing 
 the scope of a universal quantifier.  In mathematical notation we write
 \[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \]
-with the proviso `$x$ not free in~$P$.'  Isabelle's treatment of
+with the proviso ``$x$ not free in~$P$.''  Isabelle's treatment of
 substitution makes the proviso unnecessary.  The conclusion is expressed as
 \isa{P\
 \isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the
@@ -860,7 +860,7 @@
 \isacommand{apply}\ (rename_tac\ v\ w)\isanewline
 \ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w)
 \end{isabelle}
-Recall that \isa{rule_tac}\index{rule_tac|and renaming} instantiates a
+Recall that \isa{rule_tac}\index{*rule_tac!and renaming} instantiates a
 theorem with specified terms.  These terms may involve the goal's bound
 variables, but beware of referring to  variables
 like~\isa{xa}.  A future change to your theories could change the set of names
@@ -1686,7 +1686,7 @@
 
 The next step is to put
 the theorem \isa{gcd_mult_0} into a simplified form, performing the steps 
-$\gcd(1,n)=1$ and $k\times1=k$.  The \isa{simplified}\indexbold{simplified}
+$\gcd(1,n)=1$ and $k\times1=k$.  The \isaindexbold{simplified}
 attribute takes a theorem
 and returns the result of simplifying it, with respect to the default
 simplification rules:
@@ -1769,7 +1769,7 @@
 \end{isabelle}
 
 \medskip
-The \isa{rule_format}\indexbold{rule_format} directive replaces a common usage
+The \isaindexbold{rule_format} directive replaces a common usage
 of \isa{THEN}\@.  It is needed in proofs by induction when the induction formula must be
 expressed using
 \isa{\isasymlongrightarrow} and \isa{\isasymforall}.  For example, in