# HG changeset patch
# User paulson
# Date 996158582 -7200
# Node ID 7eb63f63e6c673c0db867b9dd3170851aad57eca
# Parent  e07927b980ec18f949d44e007939f4c88c941b5d
revisions and indexing

diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Ifexpr/Ifexpr.thy
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -4,7 +4,7 @@
 
 subsection{*Case Study: Boolean Expressions*}
 
-text{*\label{sec:boolex}
+text{*\label{sec:boolex}\index{boolean expressions example|(}
 The aim of this case study is twofold: it shows how to model boolean
 expressions and some algorithms for manipulating them, and it demonstrates
 the constructs introduced above.
@@ -120,7 +120,7 @@
 "norm (IF b t e) = normif b (norm t) (norm e)";
 
 text{*\noindent
-Their interplay is a bit tricky, and we leave it to the reader to develop an
+Their interplay is tricky; we leave it to you to develop an
 intuitive understanding. Fortunately, Isabelle can help us to verify that the
 transformation preserves the value of the expression:
 *}
@@ -129,7 +129,7 @@
 
 text{*\noindent
 The proof is canonical, provided we first show the following simplification
-lemma (which also helps to understand what @{term"normif"} does):
+lemma, which also helps to understand what @{term"normif"} does:
 *}
 
 lemma [simp]:
@@ -147,7 +147,7 @@
 of the theorem shown above because of the @{text"[simp]"} attribute.
 
 But how can we be sure that @{term"norm"} really produces a normal form in
-the above sense? We define a function that tests If-expressions for normality
+the above sense? We define a function that tests If-expressions for normality:
 *}
 
 consts normal :: "ifex \<Rightarrow> bool";
@@ -158,7 +158,7 @@
      (case b of CIF b \<Rightarrow> True | VIF x \<Rightarrow> True | IF x y z \<Rightarrow> False))";
 
 text{*\noindent
-and prove @{term"normal(norm b)"}. Of course, this requires a lemma about
+Now we prove @{term"normal(norm b)"}. Of course, this requires a lemma about
 normality of @{term"normif"}:
 *}
 
@@ -186,6 +186,7 @@
   some of the goals as implications (@{text"\<longrightarrow>"}) rather than
   equalities (@{text"="}).)
 \end{exercise}
+\index{boolean expressions example|)}
 *}
 (*<*)
 end
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -6,7 +6,7 @@
 }
 %
 \begin{isamarkuptext}%
-\label{sec:boolex}
+\label{sec:boolex}\index{boolean expressions example|(}
 The aim of this case study is twofold: it shows how to model boolean
 expressions and some algorithms for manipulating them, and it demonstrates
 the constructs introduced above.%
@@ -114,7 +114,7 @@
 {\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-Their interplay is a bit tricky, and we leave it to the reader to develop an
+Their interplay is tricky; we leave it to you to develop an
 intuitive understanding. Fortunately, Isabelle can help us to verify that the
 transformation preserves the value of the expression:%
 \end{isamarkuptext}%
@@ -122,7 +122,7 @@
 \begin{isamarkuptext}%
 \noindent
 The proof is canonical, provided we first show the following simplification
-lemma (which also helps to understand what \isa{normif} does):%
+lemma, which also helps to understand what \isa{normif} does:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}%
@@ -132,7 +132,7 @@
 of the theorem shown above because of the \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute.
 
 But how can we be sure that \isa{norm} really produces a normal form in
-the above sense? We define a function that tests If-expressions for normality%
+the above sense? We define a function that tests If-expressions for normality:%
 \end{isamarkuptext}%
 \isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
@@ -142,7 +142,7 @@
 \ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-and prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
+Now we prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
 normality of \isa{normif}:%
 \end{isamarkuptext}%
 \isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}%
@@ -160,7 +160,8 @@
   development to this changed requirement. (Hint: you may need to formulate
   some of the goals as implications (\isa{{\isasymlongrightarrow}}) rather than
   equalities (\isa{{\isacharequal}}).)
-\end{exercise}%
+\end{exercise}
+\index{boolean expressions example|)}%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/Translations.thy
--- a/doc-src/TutorialI/Misc/Translations.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/Translations.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -4,34 +4,34 @@
 subsection{*Syntax Translations*}
 
 text{*\label{sec:def-translations}
-\indexbold{syntax translations|(}%
-\indexbold{translations@\isacommand {translations} (command)|(}
-Isabelle offers an additional definition-like facility,
+\index{syntax translations|(}%
+\index{translations@\isacommand {translations} (command)|(}
+Isabelle offers an additional definitional facility,
 \textbf{syntax translations}.
 They resemble macros: upon parsing, the defined concept is immediately
-replaced by its definition, and this is reversed upon printing. For example,
+replaced by its definition.  This effect is reversed upon printing.  For example,
 the symbol @{text"\<noteq>"} is defined via a syntax translation:
 *}
 
 translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
 
-text{*\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
+text{*\index{$IsaEqTrans@\isasymrightleftharpoons}
 \noindent
 Internally, @{text"\<noteq>"} never appears.
 
 In addition to @{text"\<rightleftharpoons>"} there are
-@{text"\<rightharpoonup>"}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
-and @{text"\<leftharpoondown>"}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
+@{text"\<rightharpoonup>"}\index{$IsaEqTrans1@\isasymrightharpoonup}
+and @{text"\<leftharpoondown>"}\index{$IsaEqTrans2@\isasymleftharpoondown}
 for uni-directional translations, which only affect
-parsing or printing.  We do not want to cover the details of
-translations at this point.  We have mentioned the concept merely because it
-crops up occasionally: a number of HOL's built-in constructs are defined
+parsing or printing.  This tutorial will not cover the details of
+translations.  We have mentioned the concept merely because it
+crops up occasionally; a number of HOL's built-in constructs are defined
 via translations.  Translations are preferable to definitions when the new 
 concept is a trivial variation on an existing one.  For example, we
 don't need to derive new theorems about @{text"\<noteq>"}, since existing theorems
 about @{text"="} still apply.%
-\indexbold{syntax translations|)}%
-\indexbold{translations@\isacommand {translations} (command)|)}
+\index{syntax translations|)}%
+\index{translations@\isacommand {translations} (command)|)}
 *}
 
 (*<*)
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/Tree.thy
--- a/doc-src/TutorialI/Misc/Tree.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -3,7 +3,7 @@
 (*>*)
 
 text{*\noindent
-Define the datatype of binary trees
+Define the datatype of \rmindex{binary trees}:
 *}
 
 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
@@ -14,7 +14,7 @@
 "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
 
 text{*\noindent
-and a function @{term"mirror"} that mirrors a binary tree
+Define a function @{term"mirror"} that mirrors a binary tree
 by swapping subtrees recursively. Prove
 *}
 
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/case_exprs.thy
--- a/doc-src/TutorialI/Misc/case_exprs.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -4,8 +4,8 @@
 
 subsection{*Case Expressions*}
 
-text{*\label{sec:case-expressions}
-HOL also features \sdx{case}-expressions for analyzing
+text{*\label{sec:case-expressions}\index{*case expressions}%
+HOL also features \isa{case}-expressions for analyzing
 elements of a datatype. For example,
 @{term[display]"case xs of [] => 1 | y#ys => y"}
 evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if 
@@ -43,14 +43,11 @@
 subsection{*Structural Induction and Case Distinction*}
 
 text{*\label{sec:struct-ind-case}
-\indexbold{structural induction}
-\indexbold{induction!structural}
-\indexbold{case distinction}
-Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \methdx{induct_tac},
-which works for any datatype. In some cases, induction is overkill and a case
-distinction over all constructors of the datatype suffices. This is performed
-by \methdx{case_tac}. A trivial example:
+\index{case distinctions}\index{induction!structural}%
+Induction is invoked by \methdx{induct_tac}, as we have seen above; 
+it works for any datatype.  In some cases, induction is overkill and a case
+distinction over all constructors of the datatype suffices.  This is performed
+by \methdx{case_tac}.  Here is a trivial example:
 *}
 
 lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";
@@ -67,8 +64,11 @@
 text{*
 Note that we do not need to give a lemma a name if we do not intend to refer
 to it explicitly in the future.
+Other basic laws about a datatype are applied automatically during
+simplification, so no special methods are provided for them.
 
 \begin{warn}
+ 
   Induction is only allowed on free (or \isasymAnd-bound) variables that
   should not occur among the assumptions of the subgoal; see
   \S\ref{sec:ind-var-in-prems} for details. Case distinction
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/document/Translations.tex
--- a/doc-src/TutorialI/Misc/document/Translations.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Translations.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -7,33 +7,33 @@
 %
 \begin{isamarkuptext}%
 \label{sec:def-translations}
-\indexbold{syntax translations|(}%
-\indexbold{translations@\isacommand {translations} (command)|(}
-Isabelle offers an additional definition-like facility,
+\index{syntax translations|(}%
+\index{translations@\isacommand {translations} (command)|(}
+Isabelle offers an additional definitional facility,
 \textbf{syntax translations}.
 They resemble macros: upon parsing, the defined concept is immediately
-replaced by its definition, and this is reversed upon printing. For example,
+replaced by its definition.  This effect is reversed upon printing.  For example,
 the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
 \end{isamarkuptext}%
 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
-\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
+\index{$IsaEqTrans@\isasymrightleftharpoons}
 \noindent
 Internally, \isa{{\isasymnoteq}} never appears.
 
 In addition to \isa{{\isasymrightleftharpoons}} there are
-\isa{{\isasymrightharpoonup}}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
-and \isa{{\isasymleftharpoondown}}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
+\isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
+and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
 for uni-directional translations, which only affect
-parsing or printing.  We do not want to cover the details of
-translations at this point.  We have mentioned the concept merely because it
-crops up occasionally: a number of HOL's built-in constructs are defined
+parsing or printing.  This tutorial will not cover the details of
+translations.  We have mentioned the concept merely because it
+crops up occasionally; a number of HOL's built-in constructs are defined
 via translations.  Translations are preferable to definitions when the new 
 concept is a trivial variation on an existing one.  For example, we
 don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
 about \isa{{\isacharequal}} still apply.%
-\indexbold{syntax translations|)}%
-\indexbold{translations@\isacommand {translations} (command)|)}%
+\index{syntax translations|)}%
+\index{translations@\isacommand {translations} (command)|)}%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/document/Tree.tex
--- a/doc-src/TutorialI/Misc/document/Tree.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -4,12 +4,12 @@
 %
 \begin{isamarkuptext}%
 \noindent
-Define the datatype of binary trees%
+Define the datatype of \rmindex{binary trees}:%
 \end{isamarkuptext}%
 \isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-and a function \isa{mirror} that mirrors a binary tree
+Define a function \isa{mirror} that mirrors a binary tree
 by swapping subtrees recursively. Prove%
 \end{isamarkuptext}%
 \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}%
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/document/case_exprs.tex
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -6,8 +6,8 @@
 }
 %
 \begin{isamarkuptext}%
-\label{sec:case-expressions}
-HOL also features \sdx{case}-expressions for analyzing
+\label{sec:case-expressions}\index{*case expressions}%
+HOL also features \isa{case}-expressions for analyzing
 elements of a datatype. For example,
 \begin{isabelle}%
 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
@@ -54,14 +54,11 @@
 %
 \begin{isamarkuptext}%
 \label{sec:struct-ind-case}
-\indexbold{structural induction}
-\indexbold{induction!structural}
-\indexbold{case distinction}
-Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \methdx{induct_tac},
-which works for any datatype. In some cases, induction is overkill and a case
-distinction over all constructors of the datatype suffices. This is performed
-by \methdx{case_tac}. A trivial example:%
+\index{case distinctions}\index{induction!structural}%
+Induction is invoked by \methdx{induct_tac}, as we have seen above; 
+it works for any datatype.  In some cases, induction is overkill and a case
+distinction over all constructors of the datatype suffices.  This is performed
+by \methdx{case_tac}.  Here is a trivial example:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
@@ -79,8 +76,11 @@
 \begin{isamarkuptext}%
 Note that we do not need to give a lemma a name if we do not intend to refer
 to it explicitly in the future.
+Other basic laws about a datatype are applied automatically during
+simplification, so no special methods are provided for them.
 
 \begin{warn}
+ 
   Induction is only allowed on free (or \isasymAnd-bound) variables that
   should not occur among the assumptions of the subgoal; see
   \S\ref{sec:ind-var-in-prems} for details. Case distinction
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -24,6 +24,7 @@
 \begin{isamarkuptext}%
 \newcommand{\mystar}{*%
 }
+\index{arithmetic operations!for \protect\isa{nat}}%
 The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
 \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
 \sdx{div}, \sdx{mod}, \cdx{min} and
@@ -31,13 +32,15 @@
 \indexboldpos{\isasymle}{$HOL2arithrel} and
 \ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
 \isa{m\ {\isacharless}\ n}. There is even a least number operation
-\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
-Isabelle does not prove this automatically. Note that \isa{{\isadigit{1}}}
+\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}. 
+\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
+ The following needs changing with our new system of numbers.}
+Note that \isa{{\isadigit{1}}}
 and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
 \isa{Suc}-expressions. If you need the full set of numerals,
 see~\S\ref{sec:numerals}.
 
-\begin{warn}
+\begin{warn}\index{overloading}
   The constant \cdx{0} and the operations
   \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
@@ -60,23 +63,23 @@
   operations.
 \end{warn}
 
-Simple arithmetic goals are proved automatically by both \isa{auto} and the
-simplification method introduced in \S\ref{sec:Simplification}.  For
-example,%
+Both \isa{auto} and \isa{simp}
+(a method introduced below, \S\ref{sec:Simplification}) prove 
+simple arithmetic goals automatically:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-is proved automatically. The main restriction is that only addition is taken
-into account; other arithmetic operations and quantified formulae are ignored.
+For efficiency's sake, this built-in prover ignores quantified formulae and all 
+arithmetic operations apart from addition.
 
-For more complex goals, there is the special method \methdx{arith}
-(which attacks the first subgoal). It proves arithmetic goals involving the
+The method \methdx{arith} is more general.  It attempts to prove
+the first subgoal provided it is a quantifier free \textbf{linear arithmetic} formula.
+Such formulas may involve the
 usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
 \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
 and the operations
-\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
-known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
+\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. 
 For example,%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
@@ -88,7 +91,7 @@
 \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-is not even proved by \isa{arith} because the proof relies essentially
+is not proved even by \isa{arith} because the proof relies 
 on properties of multiplication.
 
 \begin{warn}
@@ -96,10 +99,9 @@
   of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
   \cdx{max} because they are first eliminated by case distinctions.
 
-  \isa{arith} is incomplete even for the restricted class of
-  linear arithmetic formulae. If divisibility plays a
+  Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
   role, it may fail to prove a valid formula, for example
-  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare in practice.
+  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare.
 \end{warn}%
 \end{isamarkuptext}%
 \end{isabellebody}%
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/document/pairs.tex
--- a/doc-src/TutorialI/Misc/document/pairs.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -18,7 +18,7 @@
 \begin{itemize}
 \item
 There is also the type \tydx{unit}, which contains exactly one
-element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
+element denoted by~\cdx{()}.  This type can be viewed
 as a degenerate product with 0 components.
 \item
 Products, like type \isa{nat}, are datatypes, which means
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/document/prime_def.tex
--- a/doc-src/TutorialI/Misc/document/prime_def.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -5,14 +5,14 @@
 \begin{isamarkuptext}%
 \begin{warn}
 A common mistake when writing definitions is to introduce extra free
-variables on the right-hand side as in the following fictitious definition:
+variables on the right-hand side.  Consider the following, flawed definition
+(where \isa{dvd} means ``divides''):
 \begin{isabelle}%
 \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
 \end{isabelle}
-where \isa{dvd} means ``divides''.
 Isabelle rejects this ``definition'' because of the extra \isa{m} on the
-right-hand side, which would introduce an inconsistency (why?). What you
-should have written is
+right-hand side, which would introduce an inconsistency (why?). 
+The correct version is
 \begin{isabelle}%
 \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
 \end{isabelle}
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/document/types.tex
--- a/doc-src/TutorialI/Misc/document/types.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -9,7 +9,7 @@
 Internally all synonyms are fully expanded.  As a consequence Isabelle's
 output never contains synonyms.  Their main purpose is to improve the
 readability of theories.  Synonyms can be used just like any other
-type:%
+type.  Here, we declare two constants of type \isa{gate}:%
 \end{isamarkuptext}%
 \isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
 \ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate%
@@ -18,19 +18,20 @@
 %
 \begin{isamarkuptext}%
 \label{sec:ConstDefinitions}\indexbold{definitions}%
-The above constants \isa{nand} and \isa{xor} are non-recursive and can
-therefore be defined directly by%
+The constants \isa{nand} and \isa{xor} above are non-recursive and can 
+be defined directly:%
 \end{isamarkuptext}%
 \isacommand{defs}\ nand{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent%
-where \commdx{defs} is a keyword and
+Here \commdx{defs} is a keyword and
 \isa{nand{\isacharunderscore}def} and \isa{xor{\isacharunderscore}def} are user-supplied names.
 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
 that must be used in constant definitions.
-Declarations and definitions can also be merged in a \commdx{constdefs} 
-command:%
+A \commdx{constdefs} command combines the effects of \isacommand{consts} and 
+\isacommand{defs}.  For instance, we can introduce \isa{nand} and \isa{xor} by a 
+single command:%
 \end{isamarkuptext}%
 \isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
 \ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -22,6 +22,7 @@
 
 text{*\newcommand{\mystar}{*%
 }
+\index{arithmetic operations!for \protect\isa{nat}}%
 The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
 \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
 \sdx{div}, \sdx{mod}, \cdx{min} and
@@ -29,13 +30,15 @@
 \indexboldpos{\isasymle}{$HOL2arithrel} and
 \ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if
 @{prop"m<n"}. There is even a least number operation
-\sdx{LEAST}\@.  For example, @{prop"(LEAST n. 1 < n) = 2"}, although
-Isabelle does not prove this automatically. Note that @{term 1}
+\sdx{LEAST}\@.  For example, @{prop"(LEAST n. 1 < n) = 2"}. 
+\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
+ The following needs changing with our new system of numbers.}
+Note that @{term 1}
 and @{term 2} are available as abbreviations for the corresponding
 @{term Suc}-expressions. If you need the full set of numerals,
 see~\S\ref{sec:numerals}.
 
-\begin{warn}
+\begin{warn}\index{overloading}
   The constant \cdx{0} and the operations
   \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
@@ -58,25 +61,25 @@
   operations.
 \end{warn}
 
-Simple arithmetic goals are proved automatically by both @{term auto} and the
-simplification method introduced in \S\ref{sec:Simplification}.  For
-example,
+Both @{text auto} and @{text simp}
+(a method introduced below, \S\ref{sec:Simplification}) prove 
+simple arithmetic goals automatically:
 *}
 
 lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
 (*<*)by(auto)(*>*)
 
 text{*\noindent
-is proved automatically. The main restriction is that only addition is taken
-into account; other arithmetic operations and quantified formulae are ignored.
+For efficiency's sake, this built-in prover ignores quantified formulae and all 
+arithmetic operations apart from addition.
 
-For more complex goals, there is the special method \methdx{arith}
-(which attacks the first subgoal). It proves arithmetic goals involving the
+The method \methdx{arith} is more general.  It attempts to prove
+the first subgoal provided it is a quantifier free \textbf{linear arithmetic} formula.
+Such formulas may involve the
 usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
 @{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
 and the operations
-@{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
-known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
+@{text"+"}, @{text"-"}, @{term min} and @{term max}. 
 For example,
 *}
 
@@ -92,7 +95,7 @@
 (*<*)oops(*>*)
 
 text{*\noindent
-is not even proved by @{text arith} because the proof relies essentially
+is not proved even by @{text arith} because the proof relies 
 on properties of multiplication.
 
 \begin{warn}
@@ -100,10 +103,9 @@
   of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
   \cdx{max} because they are first eliminated by case distinctions.
 
-  \isa{arith} is incomplete even for the restricted class of
-  linear arithmetic formulae. If divisibility plays a
+  Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
   role, it may fail to prove a valid formula, for example
-  @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare in practice.
+  @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare.
 \end{warn}
 *}
 
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/pairs.thy
--- a/doc-src/TutorialI/Misc/pairs.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/pairs.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -16,7 +16,7 @@
 \begin{itemize}
 \item
 There is also the type \tydx{unit}, which contains exactly one
-element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
+element denoted by~\cdx{()}.  This type can be viewed
 as a degenerate product with 0 components.
 \item
 Products, like type @{typ nat}, are datatypes, which means
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/prime_def.thy
--- a/doc-src/TutorialI/Misc/prime_def.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -5,12 +5,12 @@
 text{*
 \begin{warn}
 A common mistake when writing definitions is to introduce extra free
-variables on the right-hand side as in the following fictitious definition:
+variables on the right-hand side.  Consider the following, flawed definition
+(where @{text"dvd"} means ``divides''):
 @{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
-where @{text"dvd"} means ``divides''.
 Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
-right-hand side, which would introduce an inconsistency (why?). What you
-should have written is
+right-hand side, which would introduce an inconsistency (why?). 
+The correct version is
 @{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
 \end{warn}
 *}
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Misc/types.thy
--- a/doc-src/TutorialI/Misc/types.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/types.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -7,7 +7,7 @@
 Internally all synonyms are fully expanded.  As a consequence Isabelle's
 output never contains synonyms.  Their main purpose is to improve the
 readability of theories.  Synonyms can be used just like any other
-type:
+type.  Here, we declare two constants of type \isa{gate}:
 *}
 
 consts nand :: gate
@@ -16,20 +16,21 @@
 subsection{*Constant Definitions*}
 
 text{*\label{sec:ConstDefinitions}\indexbold{definitions}%
-The above constants @{term"nand"} and @{term"xor"} are non-recursive and can
-therefore be defined directly by
+The constants @{term"nand"} and @{term"xor"} above are non-recursive and can 
+be defined directly:
 *}
 
 defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
      xor_def:  "xor A B  \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
 
 text{*\noindent%
-where \commdx{defs} is a keyword and
+Here \commdx{defs} is a keyword and
 @{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names.
 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
 that must be used in constant definitions.
-Declarations and definitions can also be merged in a \commdx{constdefs} 
-command: 
+A \commdx{constdefs} command combines the effects of \isacommand{consts} and 
+\isacommand{defs}.  For instance, we can introduce @{term"nand"} and @{term"xor"} by a 
+single command: 
 *}
 
 constdefs nor :: gate
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -309,13 +309,13 @@
 
 theorem Least_equality:
      "\<lbrakk> P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> (LEAST x. P(x)) = k"
-apply (simp add: Least_def LeastM_def)
+apply (simp add: Least_def)
  
 txt{*omit maybe?
 @{subgoals[display,indent=0,margin=65]}
 *};
    
-apply (rule some_equality)
+apply (rule the_equality)
 
 txt{*
 @{subgoals[display,indent=0,margin=65]}
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Rules/Force.thy
--- a/doc-src/TutorialI/Rules/Force.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Force.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -1,6 +1,7 @@
 (* ID:         $Id$ *)
-theory Force = Divides: (*Divides rather than Main so that the first proof
-                         isn't done by the nat_divide_cancel_factor simprocs.*)
+theory Force = Main: 
+  (*Use Divides rather than Main to experiment with the first proof.
+    Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
 
 declare div_mult_self_is_m [simp del];
 
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -33,10 +33,11 @@
 The @{text 65} is the priority of the infix @{text"#"}.
 
 \begin{warn}
-  Syntax annotations are a powerful but optional feature. You
+  Syntax annotations are can be powerful, but they are difficult to master and 
+  are never necessary.  You
   could drop them from theory @{text"ToyList"} and go back to the identifiers
   @{term[source]Nil} and @{term[source]Cons}.
-  We recommend that novices avoid using
+  Novices should avoid using
   syntax annotations in their own theories.
 \end{warn}
 Next, two functions @{text"app"} and \cdx{rev} are declared:
@@ -49,7 +50,7 @@
 \noindent
 In contrast to many functional programming languages,
 Isabelle insists on explicit declarations of all functions
-(keyword \isacommand{consts}).  Apart from the declaration-before-use
+(keyword \commdx{consts}).  Apart from the declaration-before-use
 restriction, the order of items in a theory file is unconstrained. Function
 @{text"app"} is annotated with concrete syntax too. Instead of the
 prefix syntax @{text"app xs ys"} the infix
@@ -66,7 +67,7 @@
 "rev (x # xs)  = (rev xs) @ (x # [])";
 
 text{*
-\noindent
+\noindent\index{*rev (constant)|(}\index{append function|(}
 The equations for @{text"app"} and @{term"rev"} hardly need comments:
 @{text"app"} appends two lists and @{term"rev"} reverses a list.  The
 keyword \commdx{primrec} indicates that the recursion is
@@ -82,16 +83,16 @@
 % However, this is a subtle issue that we cannot discuss here further.
 
 \begin{warn}
-  As we have indicated, the requirement for total functions is not a gratuitous
-  restriction but an essential characteristic of HOL\@. It is only
+  As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
   because of totality that reasoning in HOL is comparatively easy.  More
-  generally, the philosophy in HOL is not to allow arbitrary axioms (such as
+  generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
   function definitions whose totality has not been proved) because they
   quickly lead to inconsistencies. Instead, fixed constructs for introducing
   types and functions are offered (such as \isacommand{datatype} and
   \isacommand{primrec}) which are guaranteed to preserve consistency.
 \end{warn}
 
+\index{syntax}%
 A remark about syntax.  The textual definition of a theory follows a fixed
 syntax with keywords like \isacommand{datatype} and \isacommand{end}.
 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
@@ -108,7 +109,7 @@
 
 text{*\noindent
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
-the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
+the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
 
 
 \section{An Introductory Proof}
@@ -119,27 +120,24 @@
 illustrate not just the basic proof commands but also the typical proof
 process.
 
-\subsubsection*{Main Goal: @{text"rev(rev xs) = xs"}.}
+\subsubsection*{Main Goal}
 
 Our goal is to show that reversing a list twice produces the original
-list. The input line
+list.
 *}
 
 theorem rev_rev [simp]: "rev(rev xs) = xs";
 
 txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
-\index{*simp (attribute)|bold}
 \noindent
-does several things.  It
+This \isacommand{theorem} command does several things:
 \begin{itemize}
 \item
-establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"},
+It establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"}.
 \item
-gives that theorem the name @{text"rev_rev"} by which it can be
-referred to,
+It gives that theorem the name @{text"rev_rev"}, for later reference.
 \item
-and tells Isabelle (via @{text"[simp]"}) to use the theorem (once it has been
-proved) as a simplification rule, i.e.\ all future proofs involving
+It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
 simplification will replace occurrences of @{term"rev(rev xs)"} by
 @{term"xs"}.
 
@@ -156,7 +154,7 @@
 The first three lines tell us that we are 0 steps into the proof of
 theorem @{text"rev_rev"}; for compactness reasons we rarely show these
 initial lines in this tutorial. The remaining lines display the current
-proof state.
+\rmindex{proof state}.
 Until we have finished a proof, the proof state always looks like this:
 \begin{isabelle}
 $G$\isanewline
@@ -167,7 +165,8 @@
 where $G$
 is the overall goal that we are trying to prove, and the numbered lines
 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
-establish $G$. At @{text"step 0"} there is only one subgoal, which is
+establish $G$.\index{subgoals}
+At @{text"step 0"} there is only one subgoal, which is
 identical with the overall goal.  Normally $G$ is constant and only serves as
 a reminder. Hence we rarely show it in this tutorial.
 
@@ -187,16 +186,18 @@
 (@{term[source]Cons}):
 @{subgoals[display,indent=0,margin=65]}
 
-The induction step is an example of the general format of a subgoal:
+The induction step is an example of the general format of a subgoal:\index{subgoals}
 \begin{isabelle}
 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
 ignored most of the time, or simply treated as a list of variables local to
 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
-The {\it assumptions} are the local assumptions for this subgoal and {\it
-  conclusion} is the actual proposition to be proved. Typical proof steps
-that add new assumptions are induction or case distinction. In our example
+The {\it assumptions}\index{assumptions!of subgoal}
+are the local assumptions for this subgoal and {\it
+  conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. 
+Typical proof steps
+that add new assumptions are induction and case distinction. In our example
 the only assumption is the induction hypothesis @{term"rev (rev list) =
   list"}, where @{term"list"} is a variable name chosen by Isabelle. If there
 are multiple assumptions, they are enclosed in the bracket pair
@@ -262,7 +263,7 @@
 subsubsection{*Second Lemma*}
 
 text{*
-This time the canonical proof procedure
+We again try the canonical proof procedure:
 *}
 
 lemma app_Nil2 [simp]: "xs @ [] = xs";
@@ -271,7 +272,7 @@
 
 txt{*
 \noindent
-leads to the desired message @{text"No subgoals!"}:
+It works, yielding the desired message @{text"No subgoals!"}:
 @{goals[display,indent=0]}
 We still need to confirm that the proof is now finished:
 *}
@@ -312,10 +313,11 @@
 *}
 (*<*)oops(*>*)
 
-subsubsection{*Third Lemma: @{text"(xs @ ys) @ zs = xs @ (ys @ zs)"}*}
+subsubsection{*Third Lemma*}
 
 text{*
-Abandoning the previous proof, the canonical proof procedure
+Abandoning the previous attempt, the canonical proof procedure
+succeeds without further ado.
 *}
 
 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
@@ -325,8 +327,7 @@
 
 text{*
 \noindent
-succeeds without further ado.
-Now we can prove the first lemma
+Now we can prove the first lemma:
 *}
 
 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
@@ -335,7 +336,7 @@
 done
 
 text{*\noindent
-and then prove our main theorem:
+Finally, we prove our main theorem:
 *}
 
 theorem rev_rev [simp]: "rev(rev xs) = xs";
@@ -344,8 +345,9 @@
 done
 
 text{*\noindent
-The final \isacommand{end} tells Isabelle to close the current theory because
-we are finished with its development:
+The final \commdx{end} tells Isabelle to close the current theory because
+we are finished with its development:%
+\index{*rev (constant)|)}\index{append function|)}
 *}
 
 end
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -35,10 +35,11 @@
 The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
 
 \begin{warn}
-  Syntax annotations are a powerful but optional feature. You
+  Syntax annotations are can be powerful, but they are difficult to master and 
+  are never necessary.  You
   could drop them from theory \isa{ToyList} and go back to the identifiers
   \isa{Nil} and \isa{Cons}.
-  We recommend that novices avoid using
+  Novices should avoid using
   syntax annotations in their own theories.
 \end{warn}
 Next, two functions \isa{app} and \cdx{rev} are declared:%
@@ -49,7 +50,7 @@
 \noindent
 In contrast to many functional programming languages,
 Isabelle insists on explicit declarations of all functions
-(keyword \isacommand{consts}).  Apart from the declaration-before-use
+(keyword \commdx{consts}).  Apart from the declaration-before-use
 restriction, the order of items in a theory file is unconstrained. Function
 \isa{app} is annotated with concrete syntax too. Instead of the
 prefix syntax \isa{app\ xs\ ys} the infix
@@ -64,7 +65,7 @@
 {\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
 {\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
-\noindent
+\noindent\index{*rev (constant)|(}\index{append function|(}
 The equations for \isa{app} and \isa{rev} hardly need comments:
 \isa{app} appends two lists and \isa{rev} reverses a list.  The
 keyword \commdx{primrec} indicates that the recursion is
@@ -80,16 +81,16 @@
 % However, this is a subtle issue that we cannot discuss here further.
 
 \begin{warn}
-  As we have indicated, the requirement for total functions is not a gratuitous
-  restriction but an essential characteristic of HOL\@. It is only
+  As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
   because of totality that reasoning in HOL is comparatively easy.  More
-  generally, the philosophy in HOL is not to allow arbitrary axioms (such as
+  generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
   function definitions whose totality has not been proved) because they
   quickly lead to inconsistencies. Instead, fixed constructs for introducing
   types and functions are offered (such as \isacommand{datatype} and
   \isacommand{primrec}) which are guaranteed to preserve consistency.
 \end{warn}
 
+\index{syntax}%
 A remark about syntax.  The textual definition of a theory follows a fixed
 syntax with keywords like \isacommand{datatype} and \isacommand{end}.
 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
@@ -105,7 +106,7 @@
 \begin{isamarkuptext}%
 \noindent
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
-the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
+the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
 
 
 \section{An Introductory Proof}
@@ -116,26 +117,23 @@
 illustrate not just the basic proof commands but also the typical proof
 process.
 
-\subsubsection*{Main Goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.}
+\subsubsection*{Main Goal}
 
 Our goal is to show that reversing a list twice produces the original
-list. The input line%
+list.%
 \end{isamarkuptext}%
 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \index{theorem@\isacommand {theorem} (command)|bold}%
-\index{*simp (attribute)|bold}
 \noindent
-does several things.  It
+This \isacommand{theorem} command does several things:
 \begin{itemize}
 \item
-establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
+It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
 \item
-gives that theorem the name \isa{rev{\isacharunderscore}rev} by which it can be
-referred to,
+It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference.
 \item
-and tells Isabelle (via \isa{{\isacharbrackleft}simp{\isacharbrackright}}) to use the theorem (once it has been
-proved) as a simplification rule, i.e.\ all future proofs involving
+It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
 simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
 \isa{xs}.
 
@@ -152,7 +150,7 @@
 The first three lines tell us that we are 0 steps into the proof of
 theorem \isa{rev{\isacharunderscore}rev}; for compactness reasons we rarely show these
 initial lines in this tutorial. The remaining lines display the current
-proof state.
+\rmindex{proof state}.
 Until we have finished a proof, the proof state always looks like this:
 \begin{isabelle}
 $G$\isanewline
@@ -163,7 +161,8 @@
 where $G$
 is the overall goal that we are trying to prove, and the numbered lines
 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
-establish $G$. At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
+establish $G$.\index{subgoals}
+At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
 identical with the overall goal.  Normally $G$ is constant and only serves as
 a reminder. Hence we rarely show it in this tutorial.
 
@@ -186,16 +185,18 @@
 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ {\isacharparenleft}a\ {\isacharhash}\ list{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
 \end{isabelle}
 
-The induction step is an example of the general format of a subgoal:
+The induction step is an example of the general format of a subgoal:\index{subgoals}
 \begin{isabelle}
 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
 ignored most of the time, or simply treated as a list of variables local to
 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
-The {\it assumptions} are the local assumptions for this subgoal and {\it
-  conclusion} is the actual proposition to be proved. Typical proof steps
-that add new assumptions are induction or case distinction. In our example
+The {\it assumptions}\index{assumptions!of subgoal}
+are the local assumptions for this subgoal and {\it
+  conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. 
+Typical proof steps
+that add new assumptions are induction and case distinction. In our example
 the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there
 are multiple assumptions, they are enclosed in the bracket pair
 \indexboldpos{\isasymlbrakk}{$Isabrl} and
@@ -256,14 +257,14 @@
 }
 %
 \begin{isamarkuptext}%
-This time the canonical proof procedure%
+We again try the canonical proof procedure:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-leads to the desired message \isa{No\ subgoals{\isacharbang}}:
+It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}:
 \begin{isabelle}%
 xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
 No\ subgoals{\isacharbang}%
@@ -307,11 +308,12 @@
 and the missing lemma is associativity of \isa{{\isacharat}}.%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{Third Lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
+\isamarkupsubsubsection{Third Lemma%
 }
 %
 \begin{isamarkuptext}%
-Abandoning the previous proof, the canonical proof procedure%
+Abandoning the previous attempt, the canonical proof procedure
+succeeds without further ado.%
 \end{isamarkuptext}%
 \isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
@@ -319,8 +321,7 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
-succeeds without further ado.
-Now we can prove the first lemma%
+Now we can prove the first lemma:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
@@ -328,7 +329,7 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
-and then prove our main theorem:%
+Finally, we prove our main theorem:%
 \end{isamarkuptext}%
 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
@@ -336,8 +337,9 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
-The final \isacommand{end} tells Isabelle to close the current theory because
+The final \commdx{end} tells Isabelle to close the current theory because
 we are finished with its development:%
+\index{*rev (constant)|)}\index{append function|)}%
 \end{isamarkuptext}%
 \isacommand{end}\isanewline
 \end{isabellebody}%
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/basics.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -8,10 +8,10 @@
 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
 HOL step by step following the equation
 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
-We do not assume that you are familiar with mathematical logic but that
-you are used to logical and set theoretic notation, such as covered
-in a good discrete mathematics course~\cite{Rosen-DMA}. 
-In contrast, we do assume
+We do not assume that you are familiar with mathematical logic. 
+However, we do assume that
+you are used to logical and set theoretic notation, as covered
+in a good discrete mathematics course~\cite{Rosen-DMA}, and
 that you are familiar with the basic concepts of functional
 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
 Although this tutorial initially concentrates on functional programming, do
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/fp.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -70,7 +70,7 @@
 There are two kinds of commands used during a proof: the actual proof
 commands and auxiliary commands for examining the proof state and controlling
 the display. Simple proof commands are of the form
-\commdx{apply}\isa{(method)}, where \isa{method} is typically 
+\commdx{apply}\isa{(\textit{method})}, where \textit{method} is typically 
 \isa{induct_tac} or \isa{auto}.  All such theorem proving operations
 are referred to as \bfindex{methods}, and further ones are
 introduced throughout the tutorial.  Unless stated otherwise, you may
@@ -98,8 +98,9 @@
   \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
   prints the named theorems.
 \item[Displaying types:] We have already mentioned the flag
-  \ttindex{show_types} above. It can also be useful for detecting typos in
-  formulae early on. For example, if \texttt{show_types} is set and the goal
+  \texttt{show_types} above.\index{*show_types (flag)}
+  It can also be useful for detecting misspellings in
+  formulae. For example, if \texttt{show_types} is set and the goal
   \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
 \par\noindent
 \begin{isabelle}%
@@ -124,7 +125,7 @@
   \commdx{typ} \textit{string} reads and prints the given
   string as a type in the current context.
 \item[(Re)loading theories:] When you start your interaction you must open a
-  named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle
+  named theory with the line \commdx{theory}~\isa{T~=~\dots~:}. Isabelle
   automatically loads all the required parent theories from their respective
   files (which may take a moment, unless the theories are already loaded and
   the files have not been modified).
@@ -152,6 +153,7 @@
 \section{Datatypes}
 \label{sec:datatype}
 
+\index{datatypes|(}%
 Inductive datatypes are part of almost every non-trivial application of HOL.
 First we take another look at a very important example, the datatype of
 lists, before we turn to datatypes in general. The section closes with a
@@ -161,8 +163,7 @@
 \subsection{Lists}
 
 \index{*list (type)}%
-Lists are one of the essential datatypes in computing. Readers of this
-tutorial and users of HOL need to be familiar with their basic operations.
+Lists are one of the essential datatypes in computing.  You need to be familiar with their basic operations.
 Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
 \thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
 The latter contains many further operations. For example, the functions
@@ -199,9 +200,14 @@
 Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
 the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
 just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
-  1}.  In general, \cdx{size} returns \isa{0} for all constructors
-that do not have an argument of type $t$, and for all other constructors
-\isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because
+  1}.  In general, \cdx{size} returns 
+\begin{itemize}
+\item \isa{0} for all constructors
+that do not have an argument of type $t$\\
+\item for all other constructors,
+one plus the sum of the sizes of all arguments of type~$t$.
+\end{itemize}
+Note that because
 \isa{size} is defined on every datatype, it is overloaded; on lists
 \isa{size} is also called \sdx{length}, which is not overloaded.
 Isabelle will always show \isa{size} on lists as \isa{length}.
@@ -209,6 +215,7 @@
 
 \subsection{Primitive Recursion}
 
+\index{recursion!primitive}%
 Functions on datatypes are usually defined by recursion. In fact, most of the
 time they are defined by what is called \textbf{primitive recursion}.
 The keyword \commdx{primrec} is followed by a list of
@@ -229,12 +236,14 @@
 \input{Misc/document/case_exprs.tex}
 
 \input{Ifexpr/document/Ifexpr.tex}
+\index{datatypes|)}
+
 
 \section{Some Basic Types}
 
 
 \subsection{Natural Numbers}
-\label{sec:nat}
+\label{sec:nat}\index{natural numbers}%
 \index{linear arithmetic|(}
 
 \input{Misc/document/fakenat.tex}
@@ -256,23 +265,23 @@
 A definition is simply an abbreviation, i.e.\ a new name for an existing
 construction. In particular, definitions cannot be recursive. Isabelle offers
 definitions on the level of types and terms. Those on the type level are
-called type synonyms, those on the term level are called (constant)
+called \textbf{type synonyms}; those on the term level are simply called 
 definitions.
 
 
 \subsection{Type Synonyms}
 
-\indexbold{type synonyms|(}%
-Type synonyms are similar to those found in ML\@. They are issued by a 
+\index{type synonyms|(}%
+Type synonyms are similar to those found in ML\@. They are created by a 
 \commdx{types} command:
 
 \input{Misc/document/types.tex}%
 
-Note that pattern-matching is not allowed, i.e.\ each definition must be of
+Pattern-matching is not allowed, i.e.\ each definition must be of
 the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
 Section~{\S}\ref{sec:Simp-with-Defs} explains how definitions are used
 in proofs.%
-\indexbold{type synonyms|)}
+\index{type synonyms|)}
 
 \input{Misc/document/prime_def.tex}
 
@@ -283,23 +292,16 @@
 \label{sec:definitional}
 
 As we pointed out at the beginning of the chapter, asserting arbitrary
-axioms, e.g. $f(n) = f(n) + 1$, may easily lead to contradictions. In order
+axioms such as $f(n) = f(n) + 1$ can easily lead to contradictions. In order
 to avoid this danger, this tutorial advocates the definitional rather than
-the axiomatic approach: introduce new concepts by definitions, thus
-preserving consistency. However, on the face of it, Isabelle/HOL seems to
-support many more constructs than just definitions, for example
-\isacommand{primrec}. The crucial point is that internally, everything
-(except real axioms) is reduced to a definition. For example, given some
-\isacommand{primrec} function definition, this is turned into a proper
-(nonrecursive!) definition, and the user-supplied recursion equations are
-derived as theorems from that definition. This tricky process is completely
-hidden from the user and it is not necessary to understand the details. The
-result of the definitional approach is that \isacommand{primrec} is as safe
-as pure \isacommand{defs} are, but more convenient. And this is not just the
-case for \isacommand{primrec} but also for the other commands described
-later, like \isacommand{recdef} and \isacommand{inductive}.
-This strict adherence to the definitional approach reduces the risk of 
-soundness errors inside Isabelle/HOL.
+the axiomatic approach: introduce new concepts by definitions. However,  Isabelle/HOL seems to
+support many richer definitional constructs, such as
+\isacommand{primrec}. The point is that Isabelle reduces such constructs to first principles. For example, each
+\isacommand{primrec} function definition is turned into a proper
+(nonrecursive!) definition from which the user-supplied recursion equations are
+derived as theorems.  This process is
+hidden from the user, who does not have to understand the details.  Other commands described
+later, like \isacommand{recdef} and \isacommand{inductive}, are treated similarly.  This strict adherence to the definitional approach reduces the risk of soundness errors.
 
 \chapter{More Functional Programming}
 
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/tutorial.sty
--- a/doc-src/TutorialI/tutorial.sty	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/tutorial.sty	Thu Jul 26 16:43:02 2001 +0200
@@ -50,8 +50,12 @@
 \newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@}
 \newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@}
 
-\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
-\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
+%Commented-out the original versions to see what the index looks like without them.
+%   In any event, they need to use \isa or \protect\isa rather than \texttt.
+%%\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
+%%\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
+\newcommand{\indexboldpos}[2]{#1\@}
+\newcommand{\ttindexboldpos}[2]{\isa{#1}\@}
 
 %\newtheorem{theorem}{Theorem}[section]
 \newtheorem{Exercise}{Exercise}[section]
diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Thu Jul 26 16:43:02 2001 +0200
@@ -11,8 +11,9 @@
 \makeindex
 
 \index{conditional expressions|see{\isa{if} expressions}}
-\index{primitive recursion|see{\isacommand{primrec}}}
+\index{primitive recursion|see{recursion, primitive}}
 \index{product type|see{pairs and tuples}}
+\index{structural induction|see{induction, structural}}
 \index{termination|see{functions, total}}
 \index{tuples|see{pairs and tuples}}
 \index{settings|see{flags}}