tidying the index
authorpaulson
Tue Jul 17 13:46:21 2001 +0200 (2001-07-17)
changeset 11428332347b9b942
parent 11427 3ed58bbcf4bd
child 11429 30da2f5eaf57
tidying the index
doc-src/TutorialI/Advanced/Partial.thy
doc-src/TutorialI/Advanced/advanced.tex
doc-src/TutorialI/Advanced/document/Partial.tex
doc-src/TutorialI/CodeGen/CodeGen.thy
doc-src/TutorialI/CodeGen/document/CodeGen.tex
doc-src/TutorialI/Inductive/inductive.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Makefile
doc-src/TutorialI/Misc/AdvancedInd.thy
doc-src/TutorialI/Misc/Option2.thy
doc-src/TutorialI/Misc/Translations.thy
doc-src/TutorialI/Misc/case_exprs.thy
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Misc/document/Option2.tex
doc-src/TutorialI/Misc/document/Translations.tex
doc-src/TutorialI/Misc/document/case_exprs.tex
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/document/pairs.tex
doc-src/TutorialI/Misc/document/simp.tex
doc-src/TutorialI/Misc/document/types.tex
doc-src/TutorialI/Misc/natsum.thy
doc-src/TutorialI/Misc/pairs.thy
doc-src/TutorialI/Misc/simp.thy
doc-src/TutorialI/Misc/types.thy
doc-src/TutorialI/Protocol/protocol.tex
doc-src/TutorialI/Recdef/Induction.thy
doc-src/TutorialI/Recdef/Nested2.thy
doc-src/TutorialI/Recdef/document/Induction.tex
doc-src/TutorialI/Recdef/document/Nested2.tex
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Sets/sets.tex
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Types/Axioms.thy
doc-src/TutorialI/Types/Pairs.thy
doc-src/TutorialI/Types/Records.thy
doc-src/TutorialI/Types/Typedef.thy
doc-src/TutorialI/Types/document/Axioms.tex
doc-src/TutorialI/Types/document/Pairs.tex
doc-src/TutorialI/Types/document/Typedef.tex
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/Types/types.tex
doc-src/TutorialI/basics.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/tutorial.ind
doc-src/TutorialI/tutorial.sty
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/Advanced/Partial.thy	Mon Jul 16 13:14:19 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Advanced/Partial.thy	Tue Jul 17 13:46:21 2001 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  function was applied to an argument in its domain or not. If you do
     1.5  not need to make this distinction, for example because the function is
     1.6  never used outside its domain, it is easier to work with
     1.7 -\emph{underdefined}\index{underdefined function} functions: for
     1.8 +\emph{underdefined}\index{functions!underdefined} functions: for
     1.9  certain arguments we only know that a result exists, but we do not
    1.10  know what it is. When defining functions that are normally considered
    1.11  partial, underdefinedness turns out to be a very reasonable
    1.12 @@ -143,9 +143,9 @@
    1.13  subsubsection{*The {\tt\slshape while} Combinator*}
    1.14  
    1.15  text{*If the recursive function happens to be tail recursive, its
    1.16 -definition becomes a triviality if based on the predefined \isaindexbold{while}
    1.17 +definition becomes a triviality if based on the predefined \cdx{while}
    1.18  combinator.  The latter lives in the Library theory
    1.19 -\isa{While_Combinator}, which is not part of @{text Main} but needs to
    1.20 +\thydx{While_Combinator}, which is not part of @{text Main} but needs to
    1.21  be included explicitly among the ancestor theories.
    1.22  
    1.23  Constant @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}
     2.1 --- a/doc-src/TutorialI/Advanced/advanced.tex	Mon Jul 16 13:14:19 2001 +0200
     2.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex	Tue Jul 17 13:46:21 2001 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  \input{Advanced/document/simp.tex}
     2.5  
     2.6  \section{Advanced Forms of Recursion}
     2.7 -\index{*recdef|(}
     2.8 +\index{recdef@\isacommand {recdef} (command)|(}
     2.9  
    2.10  The purpose of this section is to introduce advanced forms of
    2.11  \isacommand{recdef}: how to establish termination by means other than measure
    2.12 @@ -41,7 +41,7 @@
    2.13  \index{partial function}
    2.14  \input{Advanced/document/Partial.tex}
    2.15  
    2.16 -\index{*recdef|)}
    2.17 +\index{recdef@\isacommand {recdef} (command)|)}
    2.18  
    2.19  \section{Advanced Induction Techniques}
    2.20  \label{sec:advanced-ind}
     3.1 --- a/doc-src/TutorialI/Advanced/document/Partial.tex	Mon Jul 16 13:14:19 2001 +0200
     3.2 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Tue Jul 17 13:46:21 2001 +0200
     3.3 @@ -17,7 +17,7 @@
     3.4  function was applied to an argument in its domain or not. If you do
     3.5  not need to make this distinction, for example because the function is
     3.6  never used outside its domain, it is easier to work with
     3.7 -\emph{underdefined}\index{underdefined function} functions: for
     3.8 +\emph{underdefined}\index{functions!underdefined} functions: for
     3.9  certain arguments we only know that a result exists, but we do not
    3.10  know what it is. When defining functions that are normally considered
    3.11  partial, underdefinedness turns out to be a very reasonable
    3.12 @@ -149,9 +149,9 @@
    3.13  %
    3.14  \begin{isamarkuptext}%
    3.15  If the recursive function happens to be tail recursive, its
    3.16 -definition becomes a triviality if based on the predefined \isaindexbold{while}
    3.17 +definition becomes a triviality if based on the predefined \cdx{while}
    3.18  combinator.  The latter lives in the Library theory
    3.19 -\isa{While_Combinator}, which is not part of \isa{Main} but needs to
    3.20 +\thydx{While_Combinator}, which is not part of \isa{Main} but needs to
    3.21  be included explicitly among the ancestor theories.
    3.22  
    3.23  Constant \isa{while} is of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}
     4.1 --- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Mon Jul 16 13:14:19 2001 +0200
     4.2 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Tue Jul 17 13:46:21 2001 +0200
     4.3 @@ -110,8 +110,8 @@
     4.4  apply(induct_tac xs, simp, simp split: instr.split);
     4.5  (*<*)done(*>*)
     4.6  text{*\noindent
     4.7 -Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
     4.8 -be modified in the same way @{text simp} can. Thus the proof can be
     4.9 +Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
    4.10 +be modified in the same way as @{text simp}.  Thus the proof can be
    4.11  rewritten as
    4.12  *}
    4.13  (*<*)
     5.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Jul 16 13:14:19 2001 +0200
     5.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Tue Jul 17 13:46:21 2001 +0200
     5.3 @@ -102,8 +102,8 @@
     5.4  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
     5.5  \begin{isamarkuptext}%
     5.6  \noindent
     5.7 -Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
     5.8 -be modified in the same way \isa{simp} can. Thus the proof can be
     5.9 +Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
    5.10 +be modified in the same way as \isa{simp}.  Thus the proof can be
    5.11  rewritten as%
    5.12  \end{isamarkuptext}%
    5.13  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
     6.1 --- a/doc-src/TutorialI/Inductive/inductive.tex	Mon Jul 16 13:14:19 2001 +0200
     6.2 +++ b/doc-src/TutorialI/Inductive/inductive.tex	Tue Jul 17 13:46:21 2001 +0200
     6.3 @@ -1,5 +1,5 @@
     6.4  \chapter{Inductively Defined Sets} \label{chap:inductive}
     6.5 -\index{inductive definition|(}
     6.6 +\index{inductive definitions|(}
     6.7  
     6.8  This chapter is dedicated to the most important definition principle after
     6.9  recursive functions and datatypes: inductively defined sets.
    6.10 @@ -23,4 +23,4 @@
    6.11  
    6.12  \input{Inductive/document/AB}
    6.13  
    6.14 -\index{inductive definition|)}
    6.15 +\index{inductive definitions|)}
     7.1 --- a/doc-src/TutorialI/IsaMakefile	Mon Jul 16 13:14:19 2001 +0200
     7.2 +++ b/doc-src/TutorialI/IsaMakefile	Tue Jul 17 13:46:21 2001 +0200
     7.3 @@ -186,4 +186,4 @@
     7.4  ## clean
     7.5  
     7.6  clean:
     7.7 -	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz
     7.8 +	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz Rules/document/*.tex Sets/document/*.tex
     8.1 --- a/doc-src/TutorialI/Makefile	Mon Jul 16 13:14:19 2001 +0200
     8.2 +++ b/doc-src/TutorialI/Makefile	Tue Jul 17 13:46:21 2001 +0200
     8.3 @@ -15,6 +15,13 @@
     8.4  
     8.5  NAME = tutorial
     8.6  FILES = tutorial.tex basics.tex fp.tex appendix.tex \
     8.7 +	Advanced/advanced.tex \
     8.8 +	CTL/ctl.tex \
     8.9 +	Inductive/inductive.tex Inductive/even-example.tex \
    8.10 +	Inductive/advanced-examples.tex \
    8.11 +	Protocol/protocol.tex \
    8.12 +	Rules/rules.tex Sets/sets.tex \
    8.13 +	Types/numerics.tex Types/records.tex Types/types.tex \
    8.14  	../iman.sty ../ttbox.sty ../extra.sty \
    8.15  	isabelle.sty isabellesym.sty ../pdfsetup.sty
    8.16  
     9.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Mon Jul 16 13:14:19 2001 +0200
     9.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Jul 17 13:46:21 2001 +0200
     9.3 @@ -230,12 +230,12 @@
     9.4  identity function.
     9.5  \end{exercise}
     9.6  
     9.7 -Method @{text induct_tac} can be applied with any rule $r$
     9.8 +Method \methdx{induct_tac} can be applied with any rule $r$
     9.9  whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
    9.10  format is
    9.11  \begin{quote}
    9.12  \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
    9.13 -\end{quote}\index{*induct_tac}%
    9.14 +\end{quote}
    9.15  where $y@1, \dots, y@n$ are variables in the first subgoal.
    9.16  The conclusion of $r$ can even be an (iterated) conjunction of formulae of
    9.17  the above form in which case the application is
    10.1 --- a/doc-src/TutorialI/Misc/Option2.thy	Mon Jul 16 13:14:19 2001 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/Option2.thy	Tue Jul 17 13:46:21 2001 +0200
    10.3 @@ -4,7 +4,8 @@
    10.4  hide type option
    10.5  (*>*)
    10.6  
    10.7 -text{*\indexbold{*option}\indexbold{*None}\indexbold{*Some}
    10.8 +text{*\indexbold{*option (type)}\indexbold{*None (constant)}%
    10.9 +\indexbold{*Some (constant)}
   10.10  Our final datatype is very simple but still eminently useful:
   10.11  *}
   10.12  
    11.1 --- a/doc-src/TutorialI/Misc/Translations.thy	Mon Jul 16 13:14:19 2001 +0200
    11.2 +++ b/doc-src/TutorialI/Misc/Translations.thy	Tue Jul 17 13:46:21 2001 +0200
    11.3 @@ -4,8 +4,10 @@
    11.4  subsection{*Syntax Translations*}
    11.5  
    11.6  text{*\label{sec:def-translations}
    11.7 +\indexbold{syntax translations|(}%
    11.8 +\indexbold{translations@\isacommand {translations} (command)|(}
    11.9  Isabelle offers an additional definition-like facility,
   11.10 -\textbf{syntax translations}\indexbold{syntax translation}.
   11.11 +\textbf{syntax translations}.
   11.12  They resemble macros: upon parsing, the defined concept is immediately
   11.13  replaced by its definition, and this is reversed upon printing. For example,
   11.14  the symbol @{text"\<noteq>"} is defined via a syntax translation:
   11.15 @@ -13,7 +15,7 @@
   11.16  
   11.17  translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
   11.18  
   11.19 -text{*\indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
   11.20 +text{*\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
   11.21  \noindent
   11.22  Internally, @{text"\<noteq>"} never appears.
   11.23  
   11.24 @@ -27,7 +29,9 @@
   11.25  via translations.  Translations are preferable to definitions when the new 
   11.26  concept is a trivial variation on an existing one.  For example, we
   11.27  don't need to derive new theorems about @{text"\<noteq>"}, since existing theorems
   11.28 -about @{text"="} still apply.
   11.29 +about @{text"="} still apply.%
   11.30 +\indexbold{syntax translations|)}%
   11.31 +\indexbold{translations@\isacommand {translations} (command)|)}
   11.32  *}
   11.33  
   11.34  (*<*)
    12.1 --- a/doc-src/TutorialI/Misc/case_exprs.thy	Mon Jul 16 13:14:19 2001 +0200
    12.2 +++ b/doc-src/TutorialI/Misc/case_exprs.thy	Tue Jul 17 13:46:21 2001 +0200
    12.3 @@ -5,7 +5,7 @@
    12.4  subsection{*Case Expressions*}
    12.5  
    12.6  text{*\label{sec:case-expressions}
    12.7 -HOL also features \isaindexbold{case}-expressions for analyzing
    12.8 +HOL also features \sdx{case}-expressions for analyzing
    12.9  elements of a datatype. For example,
   12.10  @{term[display]"case xs of [] => 1 | y#ys => y"}
   12.11  evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if 
   12.12 @@ -47,10 +47,10 @@
   12.13  \indexbold{induction!structural}
   12.14  \indexbold{case distinction}
   12.15  Almost all the basic laws about a datatype are applied automatically during
   12.16 -simplification. Only induction is invoked by hand via \isaindex{induct_tac},
   12.17 +simplification. Only induction is invoked by hand via \methdx{induct_tac},
   12.18  which works for any datatype. In some cases, induction is overkill and a case
   12.19  distinction over all constructors of the datatype suffices. This is performed
   12.20 -by \isaindexbold{case_tac}. A trivial example:
   12.21 +by \methdx{case_tac}. A trivial example:
   12.22  *}
   12.23  
   12.24  lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";
    13.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Jul 16 13:14:19 2001 +0200
    13.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Jul 17 13:46:21 2001 +0200
    13.3 @@ -225,12 +225,12 @@
    13.4  identity function.
    13.5  \end{exercise}
    13.6  
    13.7 -Method \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$
    13.8 +Method \methdx{induct_tac} can be applied with any rule $r$
    13.9  whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
   13.10  format is
   13.11  \begin{quote}
   13.12  \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
   13.13 -\end{quote}\index{*induct_tac}%
   13.14 +\end{quote}
   13.15  where $y@1, \dots, y@n$ are variables in the first subgoal.
   13.16  The conclusion of $r$ can even be an (iterated) conjunction of formulae of
   13.17  the above form in which case the application is
    14.1 --- a/doc-src/TutorialI/Misc/document/Option2.tex	Mon Jul 16 13:14:19 2001 +0200
    14.2 +++ b/doc-src/TutorialI/Misc/document/Option2.tex	Tue Jul 17 13:46:21 2001 +0200
    14.3 @@ -3,7 +3,8 @@
    14.4  \def\isabellecontext{Option{\isadigit{2}}}%
    14.5  %
    14.6  \begin{isamarkuptext}%
    14.7 -\indexbold{*option}\indexbold{*None}\indexbold{*Some}
    14.8 +\indexbold{*option (type)}\indexbold{*None (constant)}%
    14.9 +\indexbold{*Some (constant)}
   14.10  Our final datatype is very simple but still eminently useful:%
   14.11  \end{isamarkuptext}%
   14.12  \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a%
    15.1 --- a/doc-src/TutorialI/Misc/document/Translations.tex	Mon Jul 16 13:14:19 2001 +0200
    15.2 +++ b/doc-src/TutorialI/Misc/document/Translations.tex	Tue Jul 17 13:46:21 2001 +0200
    15.3 @@ -7,15 +7,17 @@
    15.4  %
    15.5  \begin{isamarkuptext}%
    15.6  \label{sec:def-translations}
    15.7 +\indexbold{syntax translations|(}%
    15.8 +\indexbold{translations@\isacommand {translations} (command)|(}
    15.9  Isabelle offers an additional definition-like facility,
   15.10 -\textbf{syntax translations}\indexbold{syntax translation}.
   15.11 +\textbf{syntax translations}.
   15.12  They resemble macros: upon parsing, the defined concept is immediately
   15.13  replaced by its definition, and this is reversed upon printing. For example,
   15.14  the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
   15.15  \end{isamarkuptext}%
   15.16  \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}%
   15.17  \begin{isamarkuptext}%
   15.18 -\indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
   15.19 +\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
   15.20  \noindent
   15.21  Internally, \isa{{\isasymnoteq}} never appears.
   15.22  
   15.23 @@ -30,6 +32,8 @@
   15.24  concept is a trivial variation on an existing one.  For example, we
   15.25  don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
   15.26  about \isa{{\isacharequal}} still apply.%
   15.27 +\indexbold{syntax translations|)}%
   15.28 +\indexbold{translations@\isacommand {translations} (command)|)}%
   15.29  \end{isamarkuptext}%
   15.30  \end{isabellebody}%
   15.31  %%% Local Variables:
    16.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Jul 16 13:14:19 2001 +0200
    16.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Tue Jul 17 13:46:21 2001 +0200
    16.3 @@ -7,7 +7,7 @@
    16.4  %
    16.5  \begin{isamarkuptext}%
    16.6  \label{sec:case-expressions}
    16.7 -HOL also features \isaindexbold{case}-expressions for analyzing
    16.8 +HOL also features \sdx{case}-expressions for analyzing
    16.9  elements of a datatype. For example,
   16.10  \begin{isabelle}%
   16.11  \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
   16.12 @@ -58,10 +58,10 @@
   16.13  \indexbold{induction!structural}
   16.14  \indexbold{case distinction}
   16.15  Almost all the basic laws about a datatype are applied automatically during
   16.16 -simplification. Only induction is invoked by hand via \isaindex{induct_tac},
   16.17 +simplification. Only induction is invoked by hand via \methdx{induct_tac},
   16.18  which works for any datatype. In some cases, induction is overkill and a case
   16.19  distinction over all constructors of the datatype suffices. This is performed
   16.20 -by \isaindexbold{case_tac}. A trivial example:%
   16.21 +by \methdx{case_tac}. A trivial example:%
   16.22  \end{isamarkuptext}%
   16.23  \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
   16.24  \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
    17.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Jul 16 13:14:19 2001 +0200
    17.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Tue Jul 17 13:46:21 2001 +0200
    17.3 @@ -26,13 +26,13 @@
    17.4  }
    17.5  The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
    17.6  \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
    17.7 -\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
    17.8 -\isaindexbold{max} are predefined, as are the relations
    17.9 +\sdx{div}, \sdx{mod}, \cdx{min} and
   17.10 +\cdx{max} are predefined, as are the relations
   17.11  \indexboldpos{\isasymle}{$HOL2arithrel} and
   17.12  \ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
   17.13  \isa{m\ {\isacharless}\ n}. There is even a least number operation
   17.14 -\isaindexbold{LEAST}. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
   17.15 -Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}}
   17.16 +\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
   17.17 +Isabelle does not prove this automatically. Note that \isa{{\isadigit{1}}}
   17.18  and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
   17.19  \isa{Suc}-expressions. If you need the full set of numerals,
   17.20  see~\S\ref{sec:numerals}.
   17.21 @@ -40,8 +40,8 @@
   17.22  \begin{warn}
   17.23    The constant \cdx{0} and the operations
   17.24    \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   17.25 -  \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
   17.26 -  \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
   17.27 +  \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
   17.28 +  \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
   17.29    \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
   17.30    not just for natural numbers but at other types as well.
   17.31    For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
   17.32 @@ -76,7 +76,7 @@
   17.33  \isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
   17.34  and the operations
   17.35  \isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
   17.36 -known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
   17.37 +known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
   17.38  For example,%
   17.39  \end{isamarkuptext}%
   17.40  \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
   17.41 @@ -93,8 +93,8 @@
   17.42  
   17.43  \begin{warn}
   17.44    The running time of \isa{arith} is exponential in the number of occurrences
   17.45 -  of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
   17.46 -  \isaindexbold{max} because they are first eliminated by case distinctions.
   17.47 +  of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
   17.48 +  \cdx{max} because they are first eliminated by case distinctions.
   17.49  
   17.50    \isa{arith} is incomplete even for the restricted class of
   17.51    linear arithmetic formulae. If divisibility plays a
    18.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex	Mon Jul 16 13:14:19 2001 +0200
    18.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex	Tue Jul 17 13:46:21 2001 +0200
    18.3 @@ -3,11 +3,11 @@
    18.4  \def\isabellecontext{pairs}%
    18.5  %
    18.6  \begin{isamarkuptext}%
    18.7 -\label{sec:pairs}\indexbold{pair}
    18.8 -HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
    18.9 +\label{sec:pairs}\index{pairs and tuples}
   18.10 +HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
   18.11  \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
   18.12 -$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
   18.13 -\isaindexbold{snd}:
   18.14 +$\tau@i$. The functions \cdx{fst} and
   18.15 +\cdx{snd} extract the components of a pair:
   18.16   \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
   18.17  are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
   18.18  for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
   18.19 @@ -17,7 +17,7 @@
   18.20  Remarks:
   18.21  \begin{itemize}
   18.22  \item
   18.23 -There is also the type \isaindexbold{unit}, which contains exactly one
   18.24 +There is also the type \tydx{unit}, which contains exactly one
   18.25  element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
   18.26  as a degenerate product with 0 components.
   18.27  \item
    19.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Jul 16 13:14:19 2001 +0200
    19.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Tue Jul 17 13:46:21 2001 +0200
    19.3 @@ -57,7 +57,7 @@
    19.4  proofs seen so far could have been performed
    19.5  with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
    19.6  only the first subgoal and may thus need to be repeated --- use
    19.7 -\isaindex{simp_all} to simplify all subgoals.
    19.8 +\methdx{simp_all} to simplify all subgoals.
    19.9  Note that \isa{simp} fails if nothing changes.%
   19.10  \end{isamarkuptext}%
   19.11  %
   19.12 @@ -138,7 +138,7 @@
   19.13  Assumptions are simplified in a left-to-right fashion. If an
   19.14  assumption can help in simplifying one to the left of it, this may get
   19.15  overlooked. In such cases you have to rotate the assumptions explicitly:
   19.16 -\isacommand{apply}\isa{{\isacharparenleft}rotate{\isacharunderscore}tac}~$n$\isa{{\isacharparenright}}\indexbold{*rotate_tac}
   19.17 +\isacommand{apply}\isa{{\isacharparenleft}}\methdx{rotate_tac}~$n$\isa{{\isacharparenright}}
   19.18  causes a cyclic shift by $n$ positions from right to left, if $n$ is
   19.19  positive, and from left to right, if $n$ is negative.
   19.20  Beware that such rotations make proofs quite brittle.
   19.21 @@ -167,8 +167,8 @@
   19.22  \isacommand{lemma}\ {\isachardoublequote}xor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
   19.23  \begin{isamarkuptxt}%
   19.24  \noindent
   19.25 -Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
   19.26 -get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
   19.27 +Typically, we begin by unfolding some definitions:
   19.28 +\indexbold{definitions!unfolding}%
   19.29  \end{isamarkuptxt}%
   19.30  \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}%
   19.31  \begin{isamarkuptxt}%
   19.32 @@ -200,7 +200,7 @@
   19.33  %
   19.34  \begin{isamarkuptext}%
   19.35  \index{simplification!of let-expressions}
   19.36 -Proving a goal containing \isaindex{let}-expressions almost invariably
   19.37 +Proving a goal containing \sdx{let}-expressions almost invariably
   19.38  requires the \isa{let}-con\-structs to be expanded at some point. Since
   19.39  \isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for a predefined constant
   19.40  (called \isa{Let}), expanding \isa{let}-constructs means rewriting with
   19.41 @@ -262,13 +262,13 @@
   19.42  \begin{isabelle}%
   19.43  \ {\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}%
   19.44  \end{isabelle}
   19.45 -where \isaindexbold{split_if} is a theorem that expresses splitting of
   19.46 +where \tdx{split_if} is a theorem that expresses splitting of
   19.47  \isa{if}s. Because
   19.48  case-splitting on \isa{if}s is almost always the right proof strategy, the
   19.49  simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
   19.50  on the initial goal above.
   19.51  
   19.52 -This splitting idea generalizes from \isa{if} to \isaindex{case}.
   19.53 +This splitting idea generalizes from \isa{if} to \sdx{case}.
   19.54  Let us simplify a case analysis over lists:%
   19.55  \end{isamarkuptxt}%
   19.56  \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
   19.57 @@ -334,7 +334,7 @@
   19.58    The simplifier merely simplifies the condition of an \isa{if} but not the
   19.59    \isa{then} or \isa{else} parts. The latter are simplified only after the
   19.60    condition reduces to \isa{True} or \isa{False}, or after splitting. The
   19.61 -  same is true for \isaindex{case}-expressions: only the selector is
   19.62 +  same is true for \sdx{case}-expressions: only the selector is
   19.63    simplified at first, until either the expression reduces to one of the
   19.64    cases or it is split.
   19.65  \end{warn}\index{*split (method, attr.)|)}%
   19.66 @@ -344,7 +344,7 @@
   19.67  }
   19.68  %
   19.69  \begin{isamarkuptext}%
   19.70 -\index{arithmetic}
   19.71 +\index{linear arithmetic}
   19.72  The simplifier routinely solves a small class of linear arithmetic formulae
   19.73  (over type \isa{nat} and other numeric types): it only takes into account
   19.74  assumptions and conclusions that are relations
   19.75 @@ -367,7 +367,8 @@
   19.76  \begin{isamarkuptext}%
   19.77  \indexbold{tracing the simplifier}
   19.78  Using the simplifier effectively may take a bit of experimentation.  Set the
   19.79 -\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
   19.80 +\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} 
   19.81 +to get a better idea of what is going
   19.82  on:%
   19.83  \end{isamarkuptext}%
   19.84  \isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
    20.1 --- a/doc-src/TutorialI/Misc/document/types.tex	Mon Jul 16 13:14:19 2001 +0200
    20.2 +++ b/doc-src/TutorialI/Misc/document/types.tex	Tue Jul 17 13:46:21 2001 +0200
    20.3 @@ -5,7 +5,7 @@
    20.4  \ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
    20.5  \ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
    20.6  \begin{isamarkuptext}%
    20.7 -\noindent\indexbold{*types}%
    20.8 +\noindent
    20.9  Internally all synonyms are fully expanded.  As a consequence Isabelle's
   20.10  output never contains synonyms.  Their main purpose is to improve the
   20.11  readability of theories.  Synonyms can be used just like any other
   20.12 @@ -17,7 +17,7 @@
   20.13  }
   20.14  %
   20.15  \begin{isamarkuptext}%
   20.16 -\label{sec:ConstDefinitions}\indexbold{definition}%
   20.17 +\label{sec:ConstDefinitions}\indexbold{definitions}%
   20.18  The above constants \isa{nand} and \isa{xor} are non-recursive and can
   20.19  therefore be defined directly by%
   20.20  \end{isamarkuptext}%
   20.21 @@ -25,19 +25,20 @@
   20.22  \ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}%
   20.23  \begin{isamarkuptext}%
   20.24  \noindent%
   20.25 -where \isacommand{defs}\indexbold{*defs} is a keyword and
   20.26 +where \commdx{defs} is a keyword and
   20.27  \isa{nand{\isacharunderscore}def} and \isa{xor{\isacharunderscore}def} are user-supplied names.
   20.28  The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
   20.29  that must be used in constant definitions.
   20.30 -Declarations and definitions can also be merged%
   20.31 +Declarations and definitions can also be merged in a \commdx{constdefs} 
   20.32 +command:%
   20.33  \end{isamarkuptext}%
   20.34  \isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
   20.35  \ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
   20.36  \ \ \ \ \ \ \ \ \ \ xor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
   20.37  \ \ \ \ \ \ \ \ \ {\isachardoublequote}xor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}%
   20.38  \begin{isamarkuptext}%
   20.39 -\noindent\indexbold{*constdefs}%
   20.40 -in which case the default name of each definition is $f$\isa{{\isacharunderscore}def}, where
   20.41 +\noindent
   20.42 +The default name of each definition is $f$\isa{{\isacharunderscore}def}, where
   20.43  $f$ is the name of the defined constant.%
   20.44  \end{isamarkuptext}%
   20.45  \end{isabellebody}%
    21.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Mon Jul 16 13:14:19 2001 +0200
    21.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Tue Jul 17 13:46:21 2001 +0200
    21.3 @@ -24,13 +24,13 @@
    21.4  }
    21.5  The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
    21.6  \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
    21.7 -\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
    21.8 -\isaindexbold{max} are predefined, as are the relations
    21.9 +\sdx{div}, \sdx{mod}, \cdx{min} and
   21.10 +\cdx{max} are predefined, as are the relations
   21.11  \indexboldpos{\isasymle}{$HOL2arithrel} and
   21.12  \ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if
   21.13  @{prop"m<n"}. There is even a least number operation
   21.14 -\isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although
   21.15 -Isabelle does not prove this completely automatically. Note that @{term 1}
   21.16 +\sdx{LEAST}\@.  For example, @{prop"(LEAST n. 1 < n) = 2"}, although
   21.17 +Isabelle does not prove this automatically. Note that @{term 1}
   21.18  and @{term 2} are available as abbreviations for the corresponding
   21.19  @{term Suc}-expressions. If you need the full set of numerals,
   21.20  see~\S\ref{sec:numerals}.
   21.21 @@ -38,8 +38,8 @@
   21.22  \begin{warn}
   21.23    The constant \cdx{0} and the operations
   21.24    \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
   21.25 -  \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
   21.26 -  \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
   21.27 +  \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
   21.28 +  \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
   21.29    \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
   21.30    not just for natural numbers but at other types as well.
   21.31    For example, given the goal @{prop"x+0 = x"},
   21.32 @@ -76,7 +76,7 @@
   21.33  @{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
   21.34  and the operations
   21.35  @{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
   21.36 -known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
   21.37 +known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
   21.38  For example,
   21.39  *}
   21.40  
   21.41 @@ -97,8 +97,8 @@
   21.42  
   21.43  \begin{warn}
   21.44    The running time of @{text arith} is exponential in the number of occurrences
   21.45 -  of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
   21.46 -  \isaindexbold{max} because they are first eliminated by case distinctions.
   21.47 +  of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
   21.48 +  \cdx{max} because they are first eliminated by case distinctions.
   21.49  
   21.50    \isa{arith} is incomplete even for the restricted class of
   21.51    linear arithmetic formulae. If divisibility plays a
    22.1 --- a/doc-src/TutorialI/Misc/pairs.thy	Mon Jul 16 13:14:19 2001 +0200
    22.2 +++ b/doc-src/TutorialI/Misc/pairs.thy	Tue Jul 17 13:46:21 2001 +0200
    22.3 @@ -1,11 +1,11 @@
    22.4  (*<*)
    22.5  theory pairs = Main:;
    22.6  (*>*)
    22.7 -text{*\label{sec:pairs}\indexbold{pair}
    22.8 -HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
    22.9 +text{*\label{sec:pairs}\index{pairs and tuples}
   22.10 +HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
   22.11  \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
   22.12 -$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
   22.13 -\isaindexbold{snd}:
   22.14 +$\tau@i$. The functions \cdx{fst} and
   22.15 +\cdx{snd} extract the components of a pair:
   22.16   \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
   22.17  are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
   22.18  for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
   22.19 @@ -15,7 +15,7 @@
   22.20  Remarks:
   22.21  \begin{itemize}
   22.22  \item
   22.23 -There is also the type \isaindexbold{unit}, which contains exactly one
   22.24 +There is also the type \tydx{unit}, which contains exactly one
   22.25  element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
   22.26  as a degenerate product with 0 components.
   22.27  \item
    23.1 --- a/doc-src/TutorialI/Misc/simp.thy	Mon Jul 16 13:14:19 2001 +0200
    23.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Tue Jul 17 13:46:21 2001 +0200
    23.3 @@ -53,7 +53,7 @@
    23.4  proofs seen so far could have been performed
    23.5  with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
    23.6  only the first subgoal and may thus need to be repeated --- use
    23.7 -\isaindex{simp_all} to simplify all subgoals.
    23.8 +\methdx{simp_all} to simplify all subgoals.
    23.9  Note that @{text simp} fails if nothing changes.
   23.10  *}
   23.11  
   23.12 @@ -134,7 +134,7 @@
   23.13  Assumptions are simplified in a left-to-right fashion. If an
   23.14  assumption can help in simplifying one to the left of it, this may get
   23.15  overlooked. In such cases you have to rotate the assumptions explicitly:
   23.16 -\isacommand{apply}@{text"(rotate_tac"}~$n$@{text")"}\indexbold{*rotate_tac}
   23.17 +\isacommand{apply}@{text"("}\methdx{rotate_tac}~$n$@{text")"}
   23.18  causes a cyclic shift by $n$ positions from right to left, if $n$ is
   23.19  positive, and from left to right, if $n$ is negative.
   23.20  Beware that such rotations make proofs quite brittle.
   23.21 @@ -163,8 +163,8 @@
   23.22  lemma "xor A (\<not>A)";
   23.23  
   23.24  txt{*\noindent
   23.25 -Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
   23.26 -get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}
   23.27 +Typically, we begin by unfolding some definitions:
   23.28 +\indexbold{definitions!unfolding}
   23.29  *}
   23.30  
   23.31  apply(simp only:xor_def);
   23.32 @@ -193,7 +193,7 @@
   23.33  subsection{*Simplifying {\tt\slshape let}-Expressions*}
   23.34  
   23.35  text{*\index{simplification!of let-expressions}
   23.36 -Proving a goal containing \isaindex{let}-expressions almost invariably
   23.37 +Proving a goal containing \sdx{let}-expressions almost invariably
   23.38  requires the @{text"let"}-con\-structs to be expanded at some point. Since
   23.39  @{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for a predefined constant
   23.40  (called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
   23.41 @@ -260,13 +260,13 @@
   23.42  
   23.43  txt{*\noindent
   23.44  @{subgoals[display,indent=0]}
   23.45 -where \isaindexbold{split_if} is a theorem that expresses splitting of
   23.46 +where \tdx{split_if} is a theorem that expresses splitting of
   23.47  @{text"if"}s. Because
   23.48  case-splitting on @{text"if"}s is almost always the right proof strategy, the
   23.49  simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}
   23.50  on the initial goal above.
   23.51  
   23.52 -This splitting idea generalizes from @{text"if"} to \isaindex{case}.
   23.53 +This splitting idea generalizes from @{text"if"} to \sdx{case}.
   23.54  Let us simplify a case analysis over lists:
   23.55  *}(*<*)by simp(*>*)
   23.56  lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
   23.57 @@ -338,7 +338,7 @@
   23.58    The simplifier merely simplifies the condition of an \isa{if} but not the
   23.59    \isa{then} or \isa{else} parts. The latter are simplified only after the
   23.60    condition reduces to \isa{True} or \isa{False}, or after splitting. The
   23.61 -  same is true for \isaindex{case}-expressions: only the selector is
   23.62 +  same is true for \sdx{case}-expressions: only the selector is
   23.63    simplified at first, until either the expression reduces to one of the
   23.64    cases or it is split.
   23.65  \end{warn}\index{*split (method, attr.)|)}
   23.66 @@ -349,7 +349,7 @@
   23.67  
   23.68  subsection{*Arithmetic*}
   23.69  
   23.70 -text{*\index{arithmetic}
   23.71 +text{*\index{linear arithmetic}
   23.72  The simplifier routinely solves a small class of linear arithmetic formulae
   23.73  (over type \isa{nat} and other numeric types): it only takes into account
   23.74  assumptions and conclusions that are relations
   23.75 @@ -374,7 +374,8 @@
   23.76  subsection{*Tracing*}
   23.77  text{*\indexbold{tracing the simplifier}
   23.78  Using the simplifier effectively may take a bit of experimentation.  Set the
   23.79 -\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
   23.80 +\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} 
   23.81 +to get a better idea of what is going
   23.82  on:
   23.83  *}
   23.84  
    24.1 --- a/doc-src/TutorialI/Misc/types.thy	Mon Jul 16 13:14:19 2001 +0200
    24.2 +++ b/doc-src/TutorialI/Misc/types.thy	Tue Jul 17 13:46:21 2001 +0200
    24.3 @@ -3,7 +3,7 @@
    24.4        gate         = "bool \<Rightarrow> bool \<Rightarrow> bool"
    24.5        ('a,'b)alist = "('a \<times> 'b)list";
    24.6  
    24.7 -text{*\noindent\indexbold{*types}%
    24.8 +text{*\noindent
    24.9  Internally all synonyms are fully expanded.  As a consequence Isabelle's
   24.10  output never contains synonyms.  Their main purpose is to improve the
   24.11  readability of theories.  Synonyms can be used just like any other
   24.12 @@ -15,7 +15,7 @@
   24.13  
   24.14  subsection{*Constant Definitions*}
   24.15  
   24.16 -text{*\label{sec:ConstDefinitions}\indexbold{definition}%
   24.17 +text{*\label{sec:ConstDefinitions}\indexbold{definitions}%
   24.18  The above constants @{term"nand"} and @{term"xor"} are non-recursive and can
   24.19  therefore be defined directly by
   24.20  *}
   24.21 @@ -24,11 +24,12 @@
   24.22       xor_def:  "xor A B  \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
   24.23  
   24.24  text{*\noindent%
   24.25 -where \isacommand{defs}\indexbold{*defs} is a keyword and
   24.26 +where \commdx{defs} is a keyword and
   24.27  @{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names.
   24.28  The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
   24.29  that must be used in constant definitions.
   24.30 -Declarations and definitions can also be merged
   24.31 +Declarations and definitions can also be merged in a \commdx{constdefs} 
   24.32 +command: 
   24.33  *}
   24.34  
   24.35  constdefs nor :: gate
   24.36 @@ -36,7 +37,7 @@
   24.37            xor2 :: gate
   24.38           "xor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";
   24.39  
   24.40 -text{*\noindent\indexbold{*constdefs}%
   24.41 -in which case the default name of each definition is $f$@{text"_def"}, where
   24.42 +text{*\noindent
   24.43 +The default name of each definition is $f$@{text"_def"}, where
   24.44  $f$ is the name of the defined constant.*}
   24.45  (*<*)end(*>*)
    25.1 --- a/doc-src/TutorialI/Protocol/protocol.tex	Mon Jul 16 13:14:19 2001 +0200
    25.2 +++ b/doc-src/TutorialI/Protocol/protocol.tex	Tue Jul 17 13:46:21 2001 +0200
    25.3 @@ -1,7 +1,9 @@
    25.4  % $Id$
    25.5 -\chapter{Case Study: Verifying a Cryptographic Protocol}
    25.6 +\chapter{Case Study: Verifying a Security Protocol}
    25.7  \label{chap:crypto}
    25.8  
    25.9 +\index{protocols!security|(}
   25.10 +
   25.11  %crypto primitives 
   25.12  \def\lbb{\mathopen{\{\kern-.30em|}}
   25.13  \def\rbb{\mathclose{|\kern-.32em\}}}
   25.14 @@ -46,6 +48,7 @@
   25.15  
   25.16  \section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol}
   25.17  
   25.18 +\index{Needham-Schroeder protocol|(}%
   25.19  This protocol uses public-key cryptography. Each person has a private key, known only to
   25.20  himself, and a public key, known to everybody. If Alice wants to send Bob a secret message, she
   25.21  encrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has the
   25.22 @@ -73,7 +76,8 @@
   25.23  further property: that
   25.24  $Na$ and~$Nb$ were secrets shared by Alice and Bob.  (Many
   25.25  protocols generate such shared secrets, which can be used
   25.26 -to lessen the reliance on slow public-key operations.)  Lowe found this
   25.27 +to lessen the reliance on slow public-key operations.)  
   25.28 +Lowe\index{Lowe, Gavin|(} found this
   25.29  claim to be false: if Alice runs the protocol with someone untrustworthy
   25.30  (Charlie say), then he can start a new run with another agent (Bob say). 
   25.31  Charlie uses Alice as an oracle, masquerading as
   25.32 @@ -115,13 +119,15 @@
   25.33  will Bob.  Below, we shall look at parts of this protocol's correctness
   25.34  proof. 
   25.35  
   25.36 -In ground-breaking work, Lowe~\cite{lowe-fdr} showed how such attacks
   25.37 +In ground-breaking work, Lowe~\cite{lowe-fdr}\index{Lowe, Gavin|)}
   25.38 +showed how such attacks
   25.39  could be found automatically using a model checker.  An alternative,
   25.40  which we shall examine below, is to prove protocols correct.  Proofs
   25.41  can be done under more realistic assumptions because our model does
   25.42  not have to be finite.  The strategy is to formalize the operational
   25.43  semantics of the system and to prove security properties using rule
   25.44 -induction.
   25.45 +induction.%
   25.46 +\index{Needham-Schroeder protocol|)}
   25.47  
   25.48  
   25.49  \section{Agents and Messages}
   25.50 @@ -567,7 +573,7 @@
   25.51  \rulename{analz_Crypt_if} 
   25.52  \end{isabelle} 
   25.53  The simplifier has also used \isa{Spy_see_priK}, proved in
   25.54 -\S\ref{sec:regularity}) above, to yield \isa{Ba\ \isasymin \ bad}.
   25.55 +{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ \isasymin \ bad}.
   25.56  
   25.57  Recall that this subgoal concerns the case
   25.58  where the last message to be sent was
   25.59 @@ -634,6 +640,6 @@
   25.60  correctly~\cite{paulson-yahalom}.  Proofs of real-world protocols follow
   25.61  the strategy illustrated above, but the subgoals can
   25.62  be much bigger and there are more of them.
   25.63 -
   25.64 +\index{protocols!security|)}
   25.65  
   25.66  \endinput
    26.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Mon Jul 16 13:14:19 2001 +0200
    26.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Tue Jul 17 13:46:21 2001 +0200
    26.3 @@ -48,7 +48,7 @@
    26.4  In general, the format of invoking recursion induction is
    26.5  \begin{quote}
    26.6  \isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
    26.7 -\end{quote}\index{*induct_tac}%
    26.8 +\end{quote}\index{*induct_tac (method)}%
    26.9  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
   26.10  name of a function that takes an $n$-tuple. Usually the subgoal will
   26.11  contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
    27.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Mon Jul 16 13:14:19 2001 +0200
    27.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue Jul 17 13:46:21 2001 +0200
    27.3 @@ -77,7 +77,7 @@
    27.4  
    27.5  text{*\noindent
    27.6  or declare them globally
    27.7 -by giving them the \isaindexbold{recdef_cong} attribute as in
    27.8 +by giving them the \attrdx{recdef_cong} attribute as in
    27.9  *}
   27.10  
   27.11  declare map_cong[recdef_cong]
    28.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Jul 16 13:14:19 2001 +0200
    28.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Jul 17 13:46:21 2001 +0200
    28.3 @@ -50,7 +50,7 @@
    28.4  In general, the format of invoking recursion induction is
    28.5  \begin{quote}
    28.6  \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
    28.7 -\end{quote}\index{*induct_tac}%
    28.8 +\end{quote}\index{*induct_tac (method)}%
    28.9  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
   28.10  name of a function that takes an $n$-tuple. Usually the subgoal will
   28.11  contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
    29.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Jul 16 13:14:19 2001 +0200
    29.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Jul 17 13:46:21 2001 +0200
    29.3 @@ -74,7 +74,7 @@
    29.4  \begin{isamarkuptext}%
    29.5  \noindent
    29.6  or declare them globally
    29.7 -by giving them the \isaindexbold{recdef_cong} attribute as in%
    29.8 +by giving them the \attrdx{recdef_cong} attribute as in%
    29.9  \end{isamarkuptext}%
   29.10  \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
   29.11  \begin{isamarkuptext}%
    30.1 --- a/doc-src/TutorialI/Rules/rules.tex	Mon Jul 16 13:14:19 2001 +0200
    30.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Tue Jul 17 13:46:21 2001 +0200
    30.3 @@ -77,7 +77,7 @@
    30.4  be replaced by arbitrary formulas.  If we use the rule backwards, Isabelle
    30.5  tries to unify the current subgoal with the conclusion of the rule, which
    30.6  has the form \isa{?P\ \isasymand\ ?Q}.  (Unification is discussed below,
    30.7 -\S\ref{sec:unification}.)  If successful,
    30.8 +{\S}\ref{sec:unification}.)  If successful,
    30.9  it yields new subgoals given by the formulas assigned to 
   30.10  \isa{?P} and \isa{?Q}.
   30.11  
   30.12 @@ -175,7 +175,7 @@
   30.13  \end{isabelle}
   30.14  We assume \isa{P\ \isasymor\ Q} and
   30.15  must prove \isa{Q\ \isasymor\ P}\@.  Our first step uses the disjunction
   30.16 -elimination rule, \isa{disjE}\@.  We invoke it using \isaindex{erule}, a
   30.17 +elimination rule, \isa{disjE}\@.  We invoke it using \methdx{erule}, a
   30.18  method designed to work with elimination rules.  It looks for an assumption that
   30.19  matches the rule's first premise.  It deletes the matching assumption,
   30.20  regards the first premise as proved and returns subgoals corresponding to
   30.21 @@ -408,9 +408,9 @@
   30.22  also illustrates the \isa{intro} method: a convenient way of
   30.23  applying introduction rules.
   30.24  
   30.25 -Negation introduction deduces $\neg P$ if assuming $P$ leads to a 
   30.26 +Negation introduction deduces $\lnot P$ if assuming $P$ leads to a 
   30.27  contradiction. Negation elimination deduces any formula in the 
   30.28 -presence of $\neg P$ together with~$P$: 
   30.29 +presence of $\lnot P$ together with~$P$: 
   30.30  \begin{isabelle}
   30.31  (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
   30.32  \rulenamedx{notI}\isanewline
   30.33 @@ -418,7 +418,7 @@
   30.34  \rulenamedx{notE}
   30.35  \end{isabelle}
   30.36  %
   30.37 -Classical logic allows us to assume $\neg P$ 
   30.38 +Classical logic allows us to assume $\lnot P$ 
   30.39  when attempting to prove~$P$: 
   30.40  \begin{isabelle}
   30.41  (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
   30.42 @@ -426,7 +426,7 @@
   30.43  \end{isabelle}
   30.44  
   30.45  \index{contrapositives|(}%
   30.46 -The implications $P\imp Q$ and $\neg Q\imp\neg P$ are logically
   30.47 +The implications $P\imp Q$ and $\lnot Q\imp\lnot P$ are logically
   30.48  equivalent, and each is called the
   30.49  \textbf{contrapositive} of the other.  Four further rules support
   30.50  reasoning about contrapositives.  They differ in the placement of the
   30.51 @@ -450,7 +450,7 @@
   30.52  
   30.53  The most important of these is \isa{contrapos_np}.  It is useful
   30.54  for applying introduction rules to negated assumptions.  For instance, 
   30.55 -the assumption $\neg(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we 
   30.56 +the assumption $\lnot(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we 
   30.57  might want to use conjunction introduction on it. 
   30.58  Before we can do so, we must move that assumption so that it 
   30.59  becomes the conclusion. The following proof demonstrates this 
   30.60 @@ -586,7 +586,7 @@
   30.61  instance of~$Q$.  It is appropriate for destruction rules. 
   30.62  \item 
   30.63  Method \isa{frule\ R} is like \isa{drule\ R} except that the matching
   30.64 -assumption is not deleted.  (See \S\ref{sec:frule} below.)
   30.65 +assumption is not deleted.  (See {\S}\ref{sec:frule} below.)
   30.66  \end{itemize}
   30.67  
   30.68  Other methods apply a rule while constraining some of its
   30.69 @@ -847,7 +847,7 @@
   30.70  
   30.71  An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem
   30.72  modified using~\isa{of}, described in
   30.73 -\S\ref{sec:forward} below.   An advantage of \isa{rule_tac} is that the
   30.74 +{\S}\ref{sec:forward} below.   An advantage of \isa{rule_tac} is that the
   30.75  instantiations may refer to 
   30.76  \isasymAnd-bound variables in the current subgoal.%
   30.77  \index{substitution|)}
   30.78 @@ -1146,7 +1146,7 @@
   30.79  specify it ourselves.  Suitable methods are \isa{rule_tac}, \isa{drule_tac}
   30.80  and \isa{erule_tac}.
   30.81  
   30.82 -We have seen (just above, \S\ref{sec:frule}) a proof of this lemma:
   30.83 +We have seen (just above, {\S}\ref{sec:frule}) a proof of this lemma:
   30.84  \begin{isabelle}
   30.85  \isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\
   30.86  \isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \
   30.87 @@ -1265,13 +1265,13 @@
   30.88  
   30.89  A more challenging example illustrates how Isabelle/HOL defines the least number
   30.90  operator, which denotes the least \isa{x} satisfying~\isa{P}:%
   30.91 -\index{least number operator}
   30.92 +\index{least number operator|see{\protect\isa{LEAST}}}
   30.93  \begin{isabelle}
   30.94  (LEAST\ x.\ P\ x)\ = (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
   30.95  P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))
   30.96  \end{isabelle}
   30.97  %
   30.98 -Let us prove the counterpart of \isa{some_equality} for \isa{LEAST}\@.
   30.99 +Let us prove the counterpart of \isa{some_equality} for \sdx{LEAST}\@.
  30.100  The first step merely unfolds the definitions (\isa{LeastM} is a
  30.101  auxiliary operator):
  30.102  \begin{isabelle}
  30.103 @@ -1775,7 +1775,7 @@
  30.104  \subsection{Modifying a Theorem using {\tt\slshape of} and {\tt\slshape THEN}}
  30.105  
  30.106  Let us reproduce our examples in Isabelle.  Recall that in
  30.107 -\S\ref{sec:recdef-simplification} we declared the recursive function
  30.108 +{\S}\ref{sec:recdef-simplification} we declared the recursive function
  30.109  \isa{gcd}:\index{*gcd (constant)|(}
  30.110  \begin{isabelle}
  30.111  \isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline
  30.112 @@ -1906,7 +1906,7 @@
  30.113  \end{warn}
  30.114  
  30.115  \begin{exercise}
  30.116 -In \S\ref{sec:subst} the method \isa{subst\ mult_commute} was applied.  How
  30.117 +In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied.  How
  30.118  can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}?
  30.119  % answer  rule (mult_commute [THEN ssubst])
  30.120  \end{exercise}
  30.121 @@ -2394,7 +2394,7 @@
  30.122  %
  30.123  We use induction: \isa{gcd.induct} is the
  30.124  induction rule returned by \isa{recdef}.  We simplify using
  30.125 -rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the
  30.126 +rules proved in {\S}\ref{sec:recdef-simplification}, since rewriting by the
  30.127  definition of \isa{gcd} can loop.
  30.128  \begin{isabelle}
  30.129  \isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\
    31.1 --- a/doc-src/TutorialI/Sets/sets.tex	Mon Jul 16 13:14:19 2001 +0200
    31.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Tue Jul 17 13:46:21 2001 +0200
    31.3 @@ -324,7 +324,7 @@
    31.4  \rulenamedx{UN_E}
    31.5  \end{isabelle}
    31.6  %
    31.7 -The following built-in syntax translation (see \S\ref{sec:def-translations})
    31.8 +The following built-in syntax translation (see {\S}\ref{sec:def-translations})
    31.9  lets us express the union over a \emph{type}:
   31.10  \begin{isabelle}
   31.11  \ \ \ \ \
   31.12 @@ -368,7 +368,7 @@
   31.13  Isabelle uses logical equivalences such as those above in automatic proof. 
   31.14  Unions, intersections and so forth are not simply replaced by their
   31.15  definitions.  Instead, membership tests are simplified.  For example,  $x\in
   31.16 -A\cup B$ is replaced by $x\in A\vee x\in B$.
   31.17 +A\cup B$ is replaced by $x\in A\lor x\in B$.
   31.18  
   31.19  The internal form of a comprehension involves the constant  
   31.20  \cdx{Collect},
   31.21 @@ -742,7 +742,7 @@
   31.22  
   31.23  \subsection{The Reflexive and Transitive Closure}
   31.24  
   31.25 -\index{closure!reflexive and transitive|(}%
   31.26 +\index{reflexive and transitive closure|(}%
   31.27  The \textbf{reflexive and transitive closure} of the
   31.28  relation~\isa{r} is written with a
   31.29  postfix syntax.  In ASCII we write \isa{r\isacharcircum*} and in
   31.30 @@ -871,7 +871,7 @@
   31.31  \isa{auto}, \isa{fast} and \isa{best}.  Section~\ref{sec:products} will discuss proof
   31.32  techniques for ordered pairs in more detail.
   31.33  \end{warn}
   31.34 -\index{relations|)}\index{closure!reflexive and transitive|)}
   31.35 +\index{relations|)}\index{reflexive and transitive closure|)}
   31.36  
   31.37  
   31.38  \section{Well-Founded Relations and Induction}
   31.39 @@ -902,7 +902,7 @@
   31.40  complex recursive function definition or induction.  The induction rule
   31.41  returned by
   31.42  \isacommand{recdef} is good enough for most purposes.  We use an explicit
   31.43 -well-founded induction only in \S\ref{sec:CTL-revisited}.
   31.44 +well-founded induction only in {\S}\ref{sec:CTL-revisited}.
   31.45  \end{warn}
   31.46  
   31.47  Isabelle/HOL declares \cdx{less_than} as a relation object, 
   31.48 @@ -960,11 +960,11 @@
   31.49  \end{isabelle}
   31.50  
   31.51  These constructions can be used in a
   31.52 -\textbf{recdef} declaration (\S\ref{sec:recdef-simplification}) to define
   31.53 +\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define
   31.54  the well-founded relation used to prove termination.
   31.55  
   31.56  The \bfindex{multiset ordering}, useful for hard termination proofs, is
   31.57 -available in the Library.  Baader and Nipkow \cite[\S2.5]{Baader-Nipkow}
   31.58 +available in the Library.  Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow}
   31.59  discuss it. 
   31.60  
   31.61  \medskip
   31.62 @@ -1014,7 +1014,7 @@
   31.63  
   31.64  \begin{warn}
   31.65  Casual readers should skip the rest of this section.  We use fixed point
   31.66 -operators only in \S\ref{sec:VMC}.
   31.67 +operators only in {\S}\ref{sec:VMC}.
   31.68  \end{warn}
   31.69  
   31.70  The theory applies only to monotonic functions.\index{monotone functions|bold} 
   31.71 @@ -1065,7 +1065,8 @@
   31.72  gfp\ f%
   31.73  \rulename{coinduct}
   31.74  \end{isabelle}
   31.75 -A \bfindex{bisimulation} is perhaps the best-known concept defined as a
   31.76 +A \textbf{bisimulation}\index{bisimulations} 
   31.77 +is perhaps the best-known concept defined as a
   31.78  greatest fixed point.  Exhibiting a bisimulation to prove the equality of
   31.79  two agents in a process algebra is an example of coinduction.
   31.80  The coinduction rule can be strengthened in various ways; see 
    32.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Mon Jul 16 13:14:19 2001 +0200
    32.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Jul 17 13:46:21 2001 +0200
    32.3 @@ -13,8 +13,9 @@
    32.4                   | Cons 'a "'a list"            (infixr "#" 65);
    32.5  
    32.6  text{*\noindent
    32.7 -The datatype\index{*datatype} \isaindexbold{list} introduces two
    32.8 -constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
    32.9 +\index{datatype@\isacommand {datatype} (command)}
   32.10 +The datatype \tydx{list} introduces two
   32.11 +constructors \cdx{Nil} and \cdx{Cons}, the
   32.12  empty~list and the operator that adds an element to the front of a list. For
   32.13  example, the term \isa{Cons True (Cons False Nil)} is a value of
   32.14  type @{typ"bool list"}, namely the list with the elements @{term"True"} and
   32.15 @@ -25,7 +26,8 @@
   32.16  @{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
   32.17  alternative syntax is the standard syntax. Thus the list \isa{Cons True
   32.18  (Cons False Nil)} becomes @{term"True # False # []"}. The annotation
   32.19 -\isacommand{infixr}\indexbold{*infixr} means that @{text"#"} associates to
   32.20 +\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 
   32.21 +means that @{text"#"} associates to
   32.22  the right, i.e.\ the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
   32.23  and not as @{text"(x # y) # z"}.
   32.24  The @{text 65} is the priority of the infix @{text"#"}.
   32.25 @@ -37,7 +39,7 @@
   32.26    We recommend that novices avoid using
   32.27    syntax annotations in their own theories.
   32.28  \end{warn}
   32.29 -Next, two functions @{text"app"} and \isaindexbold{rev} are declared:
   32.30 +Next, two functions @{text"app"} and \cdx{rev} are declared:
   32.31  *}
   32.32  
   32.33  consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   (infixr "@" 65)
   32.34 @@ -67,11 +69,11 @@
   32.35  \noindent
   32.36  The equations for @{text"app"} and @{term"rev"} hardly need comments:
   32.37  @{text"app"} appends two lists and @{term"rev"} reverses a list.  The
   32.38 -keyword \isacommand{primrec}\index{*primrec} indicates that the recursion is
   32.39 +keyword \commdx{primrec} indicates that the recursion is
   32.40  of a particularly primitive kind where each recursive call peels off a datatype
   32.41  constructor from one of the arguments.  Thus the
   32.42  recursion always terminates, i.e.\ the function is \textbf{total}.
   32.43 -\index{total function}
   32.44 +\index{functions!total}
   32.45  
   32.46  The termination requirement is absolutely essential in HOL, a logic of total
   32.47  functions. If we were to drop it, inconsistencies would quickly arise: the
   32.48 @@ -125,7 +127,8 @@
   32.49  
   32.50  theorem rev_rev [simp]: "rev(rev xs) = xs";
   32.51  
   32.52 -txt{*\index{*theorem|bold}\index{*simp (attribute)|bold}
   32.53 +txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
   32.54 +\index{*simp (attribute)|bold}
   32.55  \noindent
   32.56  does several things.  It
   32.57  \begin{itemize}
   32.58 @@ -170,14 +173,15 @@
   32.59  
   32.60  Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively
   32.61  defined functions are best established by induction. In this case there is
   32.62 -not much choice except to induct on @{term"xs"}:
   32.63 +nothing obvious except induction on @{term"xs"}:
   32.64  *}
   32.65  
   32.66  apply(induct_tac xs);
   32.67  
   32.68 -txt{*\noindent\index{*induct_tac}%
   32.69 +txt{*\noindent\index{*induct_tac (method)}%
   32.70  This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
   32.71 -@{term"tac"} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
   32.72 +@{term"tac"} stands for \textbf{tactic},\index{tactics}
   32.73 +a synonym for ``theorem proving function''.
   32.74  By default, induction acts on the first subgoal. The new proof state contains
   32.75  two subgoals, namely the base case (@{term[source]Nil}) and the induction step
   32.76  (@{term[source]Cons}):
   32.77 @@ -217,21 +221,20 @@
   32.78  oops
   32.79  (*>*)
   32.80  
   32.81 -subsubsection{*First Lemma: @{text"rev(xs @ ys) = (rev ys) @ (rev xs)"}*}
   32.82 +subsubsection{*First Lemma*}
   32.83  
   32.84  text{*
   32.85 -After abandoning the above proof attempt\indexbold{abandon
   32.86 -proof}\indexbold{proof!abandon} (at the shell level type
   32.87 -\isacommand{oops}\indexbold{*oops}) we start a new proof:
   32.88 +\indexbold{abandoning a proof}\indexbold{proofs!abandoning}
   32.89 +After abandoning the above proof attempt (at the shell level type
   32.90 +\commdx{oops}) we start a new proof:
   32.91  *}
   32.92  
   32.93  lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
   32.94  
   32.95 -txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
   32.96 -\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
   32.97 +txt{*\noindent The keywords \commdx{theorem} and
   32.98 +\commdx{lemma} are interchangeable and merely indicate
   32.99  the importance we attach to a proposition.  Therefore we use the words
  32.100 -\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
  32.101 -interchangeably, too.
  32.102 +\emph{theorem} and \emph{lemma} pretty much interchangeably, too.
  32.103  
  32.104  There are two variables that we could induct on: @{term"xs"} and
  32.105  @{term"ys"}. Because @{text"@"} is defined by recursion on
  32.106 @@ -256,7 +259,7 @@
  32.107  oops
  32.108  (*>*)
  32.109  
  32.110 -subsubsection{*Second Lemma: @{text"xs @ [] = xs"}*}
  32.111 +subsubsection{*Second Lemma*}
  32.112  
  32.113  text{*
  32.114  This time the canonical proof procedure
  32.115 @@ -275,8 +278,8 @@
  32.116  
  32.117  done
  32.118  
  32.119 -text{*\noindent\indexbold{done}%
  32.120 -As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
  32.121 +text{*\noindent
  32.122 +As a result of that final \commdx{done}, Isabelle associates the lemma just proved
  32.123  with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
  32.124  if it is obvious from the context that the proof is finished.
  32.125  
    33.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Jul 16 13:14:19 2001 +0200
    33.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Jul 17 13:46:21 2001 +0200
    33.3 @@ -15,8 +15,9 @@
    33.4  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}%
    33.5  \begin{isamarkuptext}%
    33.6  \noindent
    33.7 -The datatype\index{*datatype} \isaindexbold{list} introduces two
    33.8 -constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
    33.9 +\index{datatype@\isacommand {datatype} (command)}
   33.10 +The datatype \tydx{list} introduces two
   33.11 +constructors \cdx{Nil} and \cdx{Cons}, the
   33.12  empty~list and the operator that adds an element to the front of a list. For
   33.13  example, the term \isa{Cons True (Cons False Nil)} is a value of
   33.14  type \isa{bool\ list}, namely the list with the elements \isa{True} and
   33.15 @@ -27,7 +28,8 @@
   33.16  \isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
   33.17  alternative syntax is the standard syntax. Thus the list \isa{Cons True
   33.18  (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
   33.19 -\isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
   33.20 +\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 
   33.21 +means that \isa{{\isacharhash}} associates to
   33.22  the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
   33.23  and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
   33.24  The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
   33.25 @@ -39,7 +41,7 @@
   33.26    We recommend that novices avoid using
   33.27    syntax annotations in their own theories.
   33.28  \end{warn}
   33.29 -Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
   33.30 +Next, two functions \isa{app} and \cdx{rev} are declared:%
   33.31  \end{isamarkuptext}%
   33.32  \isacommand{consts}\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharat}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\isanewline
   33.33  \ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
   33.34 @@ -65,11 +67,11 @@
   33.35  \noindent
   33.36  The equations for \isa{app} and \isa{rev} hardly need comments:
   33.37  \isa{app} appends two lists and \isa{rev} reverses a list.  The
   33.38 -keyword \isacommand{primrec}\index{*primrec} indicates that the recursion is
   33.39 +keyword \commdx{primrec} indicates that the recursion is
   33.40  of a particularly primitive kind where each recursive call peels off a datatype
   33.41  constructor from one of the arguments.  Thus the
   33.42  recursion always terminates, i.e.\ the function is \textbf{total}.
   33.43 -\index{total function}
   33.44 +\index{functions!total}
   33.45  
   33.46  The termination requirement is absolutely essential in HOL, a logic of total
   33.47  functions. If we were to drop it, inconsistencies would quickly arise: the
   33.48 @@ -121,7 +123,8 @@
   33.49  \end{isamarkuptext}%
   33.50  \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
   33.51  \begin{isamarkuptxt}%
   33.52 -\index{*theorem|bold}\index{*simp (attribute)|bold}
   33.53 +\index{theorem@\isacommand {theorem} (command)|bold}%
   33.54 +\index{*simp (attribute)|bold}
   33.55  \noindent
   33.56  does several things.  It
   33.57  \begin{itemize}
   33.58 @@ -166,13 +169,14 @@
   33.59  
   33.60  Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively
   33.61  defined functions are best established by induction. In this case there is
   33.62 -not much choice except to induct on \isa{xs}:%
   33.63 +nothing obvious except induction on \isa{xs}:%
   33.64  \end{isamarkuptxt}%
   33.65  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
   33.66  \begin{isamarkuptxt}%
   33.67 -\noindent\index{*induct_tac}%
   33.68 +\noindent\index{*induct_tac (method)}%
   33.69  This tells Isabelle to perform induction on variable \isa{xs}. The suffix
   33.70 -\isa{tac} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
   33.71 +\isa{tac} stands for \textbf{tactic},\index{tactics}
   33.72 +a synonym for ``theorem proving function''.
   33.73  By default, induction acts on the first subgoal. The new proof state contains
   33.74  two subgoals, namely the base case (\isa{Nil}) and the induction step
   33.75  (\isa{Cons}):
   33.76 @@ -214,21 +218,20 @@
   33.77  In order to simplify this subgoal further, a lemma suggests itself.%
   33.78  \end{isamarkuptxt}%
   33.79  %
   33.80 -\isamarkupsubsubsection{First Lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}%
   33.81 +\isamarkupsubsubsection{First Lemma%
   33.82  }
   33.83  %
   33.84  \begin{isamarkuptext}%
   33.85 -After abandoning the above proof attempt\indexbold{abandon
   33.86 -proof}\indexbold{proof!abandon} (at the shell level type
   33.87 -\isacommand{oops}\indexbold{*oops}) we start a new proof:%
   33.88 +\indexbold{abandoning a proof}\indexbold{proofs!abandoning}
   33.89 +After abandoning the above proof attempt (at the shell level type
   33.90 +\commdx{oops}) we start a new proof:%
   33.91  \end{isamarkuptext}%
   33.92  \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}%
   33.93  \begin{isamarkuptxt}%
   33.94 -\noindent The keywords \isacommand{theorem}\index{*theorem} and
   33.95 -\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
   33.96 +\noindent The keywords \commdx{theorem} and
   33.97 +\commdx{lemma} are interchangeable and merely indicate
   33.98  the importance we attach to a proposition.  Therefore we use the words
   33.99 -\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
  33.100 -interchangeably, too.
  33.101 +\emph{theorem} and \emph{lemma} pretty much interchangeably, too.
  33.102  
  33.103  There are two variables that we could induct on: \isa{xs} and
  33.104  \isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
  33.105 @@ -249,7 +252,7 @@
  33.106  embarking on the proof of a lemma usually remains implicit.%
  33.107  \end{isamarkuptxt}%
  33.108  %
  33.109 -\isamarkupsubsubsection{Second Lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}%
  33.110 +\isamarkupsubsubsection{Second Lemma%
  33.111  }
  33.112  %
  33.113  \begin{isamarkuptext}%
  33.114 @@ -269,8 +272,8 @@
  33.115  \end{isamarkuptxt}%
  33.116  \isacommand{done}%
  33.117  \begin{isamarkuptext}%
  33.118 -\noindent\indexbold{done}%
  33.119 -As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
  33.120 +\noindent
  33.121 +As a result of that final \commdx{done}, Isabelle associates the lemma just proved
  33.122  with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
  33.123  if it is obvious from the context that the proof is finished.
  33.124  
    34.1 --- a/doc-src/TutorialI/Types/Axioms.thy	Mon Jul 16 13:14:19 2001 +0200
    34.2 +++ b/doc-src/TutorialI/Types/Axioms.thy	Tue Jul 17 13:46:21 2001 +0200
    34.3 @@ -212,7 +212,7 @@
    34.4  wford}. Such intersections need not be given a new name but can be created on
    34.5  the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
    34.6  represents the intersection of the $C@i$. Such an expression is called a
    34.7 -\bfindex{sort}, and sorts can appear in most places where we have only shown
    34.8 +\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
    34.9  classes so far, for example in type constraints: @{text"'a::{linord,wford}"}.
   34.10  In fact, @{text"'a::C"} is short for @{text"'a::{C}"}.
   34.11  However, we do not pursue this rarefied concept further.
    35.1 --- a/doc-src/TutorialI/Types/Pairs.thy	Mon Jul 16 13:14:19 2001 +0200
    35.2 +++ b/doc-src/TutorialI/Types/Pairs.thy	Tue Jul 17 13:46:21 2001 +0200
    35.3 @@ -1,9 +1,9 @@
    35.4  (*<*)theory Pairs = Main:(*>*)
    35.5  
    35.6 -section{*Pairs*}
    35.7 +section{*Pairs and Tuples*}
    35.8  
    35.9  text{*\label{sec:products}
   35.10 -Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
   35.11 +Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
   35.12  repertoire of operations: pairing and the two projections @{term fst} and
   35.13  @{term snd}. In any non-trivial application of pairs you will find that this
   35.14  quickly leads to unreadable formulae involving nests of projections. This
    36.1 --- a/doc-src/TutorialI/Types/Records.thy	Mon Jul 16 13:14:19 2001 +0200
    36.2 +++ b/doc-src/TutorialI/Types/Records.thy	Tue Jul 17 13:46:21 2001 +0200
    36.3 @@ -19,6 +19,7 @@
    36.4   following theorems:
    36.5  *}
    36.6  
    36.7 +
    36.8  thm "point.simps"
    36.9  text {*
   36.10  Incomprehensible equations: the selectors Xcoord and Ycoord, also "more";
    37.1 --- a/doc-src/TutorialI/Types/Typedef.thy	Mon Jul 16 13:14:19 2001 +0200
    37.2 +++ b/doc-src/TutorialI/Types/Typedef.thy	Tue Jul 17 13:46:21 2001 +0200
    37.3 @@ -17,12 +17,14 @@
    37.4  subsection{*Declaring New Types*}
    37.5  
    37.6  text{*\label{sec:typedecl}
    37.7 -The most trivial way of introducing a new type is by a \bfindex{type
    37.8 +\index{types!declaring|(}%
    37.9 +\index{typedecl@\isacommand {typedecl} (command)}%
   37.10 +The most trivial way of introducing a new type is by a \textbf{type
   37.11  declaration}: *}
   37.12  
   37.13  typedecl my_new_type
   37.14  
   37.15 -text{*\noindent\indexbold{*typedecl}%
   37.16 +text{*\noindent
   37.17  This does not define @{typ my_new_type} at all but merely introduces its
   37.18  name. Thus we know nothing about this type, except that it is
   37.19  non-empty. Such declarations without definitions are
   37.20 @@ -48,13 +50,16 @@
   37.21  axioms, in which case you will be able to prove everything but it will mean
   37.22  nothing.  In the example above, the axiomatic approach is
   37.23  unnecessary: a one-element type called @{typ unit} is already defined in HOL.
   37.24 +\index{types!declaring|)}
   37.25  *}
   37.26  
   37.27  subsection{*Defining New Types*}
   37.28  
   37.29  text{*\label{sec:typedef}
   37.30 -Now we come to the most general method of safely introducing a new type, the
   37.31 -\bfindex{type definition}. All other methods, for example
   37.32 +\index{types!defining|(}%
   37.33 +\index{typedecl@\isacommand {typedef} (command)|(}%
   37.34 +Now we come to the most general means of safely introducing a new type, the
   37.35 +\textbf{type definition}. All other means, for example
   37.36  \isacommand{datatype}, are based on it. The principle is extremely simple:
   37.37  any non-empty subset of an existing type can be turned into a new type.  Thus
   37.38  a type definition is merely a notational device: you introduce a new name for
   37.39 @@ -70,7 +75,7 @@
   37.40  
   37.41  typedef three = "{n. n \<le> 2}"
   37.42  
   37.43 -txt{*\noindent\indexbold{*typedef}%
   37.44 +txt{*\noindent
   37.45  In order to enforce that the representing set on the right-hand side is
   37.46  non-empty, this definition actually starts a proof to that effect:
   37.47  @{subgoals[display,indent=0]}
   37.48 @@ -276,7 +281,9 @@
   37.49  \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
   37.50  \end{enumerate}
   37.51  You can now forget about the representation and work solely in terms of the
   37.52 -abstract functions $F$ and properties $P$.
   37.53 +abstract functions $F$ and properties $P$.%
   37.54 +\index{typedecl@\isacommand {typedef} (command)|)}%
   37.55 +\index{types!defining|)}
   37.56  *}
   37.57  
   37.58  (*<*)end(*>*)
    38.1 --- a/doc-src/TutorialI/Types/document/Axioms.tex	Mon Jul 16 13:14:19 2001 +0200
    38.2 +++ b/doc-src/TutorialI/Types/document/Axioms.tex	Tue Jul 17 13:46:21 2001 +0200
    38.3 @@ -204,7 +204,7 @@
    38.4  be viewed as the intersection of the two classes \isa{linord} and \isa{wford}. Such intersections need not be given a new name but can be created on
    38.5  the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
    38.6  represents the intersection of the $C@i$. Such an expression is called a
    38.7 -\bfindex{sort}, and sorts can appear in most places where we have only shown
    38.8 +\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
    38.9  classes so far, for example in type constraints: \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}linord{\isacharcomma}wford{\isacharbraceright}}.
   38.10  In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}C} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}C{\isacharbraceright}}.
   38.11  However, we do not pursue this rarefied concept further.
    39.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex	Mon Jul 16 13:14:19 2001 +0200
    39.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex	Tue Jul 17 13:46:21 2001 +0200
    39.3 @@ -2,12 +2,12 @@
    39.4  \begin{isabellebody}%
    39.5  \def\isabellecontext{Pairs}%
    39.6  %
    39.7 -\isamarkupsection{Pairs%
    39.8 +\isamarkupsection{Pairs and Tuples%
    39.9  }
   39.10  %
   39.11  \begin{isamarkuptext}%
   39.12  \label{sec:products}
   39.13 -Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
   39.14 +Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
   39.15  repertoire of operations: pairing and the two projections \isa{fst} and
   39.16  \isa{snd}. In any non-trivial application of pairs you will find that this
   39.17  quickly leads to unreadable formulae involving nests of projections. This
    40.1 --- a/doc-src/TutorialI/Types/document/Typedef.tex	Mon Jul 16 13:14:19 2001 +0200
    40.2 +++ b/doc-src/TutorialI/Types/document/Typedef.tex	Tue Jul 17 13:46:21 2001 +0200
    40.3 @@ -23,12 +23,14 @@
    40.4  %
    40.5  \begin{isamarkuptext}%
    40.6  \label{sec:typedecl}
    40.7 -The most trivial way of introducing a new type is by a \bfindex{type
    40.8 +\index{types!declaring|(}%
    40.9 +\index{typedecl@\isacommand {typedecl} (command)}%
   40.10 +The most trivial way of introducing a new type is by a \textbf{type
   40.11  declaration}:%
   40.12  \end{isamarkuptext}%
   40.13  \isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type%
   40.14  \begin{isamarkuptext}%
   40.15 -\noindent\indexbold{*typedecl}%
   40.16 +\noindent
   40.17  This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its
   40.18  name. Thus we know nothing about this type, except that it is
   40.19  non-empty. Such declarations without definitions are
   40.20 @@ -52,7 +54,8 @@
   40.21  of your development. It is extremely easy to write down contradictory sets of
   40.22  axioms, in which case you will be able to prove everything but it will mean
   40.23  nothing.  In the example above, the axiomatic approach is
   40.24 -unnecessary: a one-element type called \isa{unit} is already defined in HOL.%
   40.25 +unnecessary: a one-element type called \isa{unit} is already defined in HOL.
   40.26 +\index{types!declaring|)}%
   40.27  \end{isamarkuptext}%
   40.28  %
   40.29  \isamarkupsubsection{Defining New Types%
   40.30 @@ -60,8 +63,10 @@
   40.31  %
   40.32  \begin{isamarkuptext}%
   40.33  \label{sec:typedef}
   40.34 -Now we come to the most general method of safely introducing a new type, the
   40.35 -\bfindex{type definition}. All other methods, for example
   40.36 +\index{types!defining|(}%
   40.37 +\index{typedecl@\isacommand {typedef} (command)|(}%
   40.38 +Now we come to the most general means of safely introducing a new type, the
   40.39 +\textbf{type definition}. All other means, for example
   40.40  \isacommand{datatype}, are based on it. The principle is extremely simple:
   40.41  any non-empty subset of an existing type can be turned into a new type.  Thus
   40.42  a type definition is merely a notational device: you introduce a new name for
   40.43 @@ -76,7 +81,7 @@
   40.44  \end{isamarkuptext}%
   40.45  \isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}%
   40.46  \begin{isamarkuptxt}%
   40.47 -\noindent\indexbold{*typedef}%
   40.48 +\noindent
   40.49  In order to enforce that the representing set on the right-hand side is
   40.50  non-empty, this definition actually starts a proof to that effect:
   40.51  \begin{isabelle}%
   40.52 @@ -274,6 +279,8 @@
   40.53  \end{enumerate}
   40.54  You can now forget about the representation and work solely in terms of the
   40.55  abstract functions $F$ and properties $P$.%
   40.56 +\index{typedecl@\isacommand {typedef} (command)|)}%
   40.57 +\index{types!defining|)}%
   40.58  \end{isamarkuptext}%
   40.59  \end{isabellebody}%
   40.60  %%% Local Variables:
    41.1 --- a/doc-src/TutorialI/Types/numerics.tex	Mon Jul 16 13:14:19 2001 +0200
    41.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Tue Jul 17 13:46:21 2001 +0200
    41.3 @@ -76,7 +76,7 @@
    41.4  \end{warn}
    41.5  
    41.6  \begin{warn}
    41.7 -\index{recdef@\protect\isacommand{recdef} (command)!and numeric literals}  
    41.8 +\index{recdef@\isacommand {recdef} (command)!and numeric literals}  
    41.9  Numeric literals are not constructors and therefore
   41.10  must not be used in patterns.  For example, this declaration is
   41.11  rejected:
   41.12 @@ -434,7 +434,7 @@
   41.13  Type \isa{real} is only available in the logic HOL-Real, which
   41.14  is  HOL extended with the rather substantial development of the real
   41.15  numbers.  Base your theory upon theory
   41.16 -\isa{Real}, not the usual \isa{Main}.%
   41.17 +\thydx{Real}, not the usual \isa{Main}.%
   41.18  \index{real numbers|)}\index{*real (type)|)}
   41.19  Launch Isabelle using the command 
   41.20  \begin{verbatim}
    42.1 --- a/doc-src/TutorialI/Types/types.tex	Mon Jul 16 13:14:19 2001 +0200
    42.2 +++ b/doc-src/TutorialI/Types/types.tex	Tue Jul 17 13:46:21 2001 +0200
    42.3 @@ -23,16 +23,16 @@
    42.4  
    42.5  \input{Types/numerics}
    42.6  
    42.7 -\index{pair|(}
    42.8 +\index{pairs and tuples|(}
    42.9  \input{Types/document/Pairs}
   42.10 -\index{pair|)}
   42.11 +\index{pairs and tuples|)}
   42.12  
   42.13  \input{Types/records}
   42.14  
   42.15  
   42.16  \section{Axiomatic Type Classes}
   42.17  \label{sec:axclass}
   42.18 -\index{axiomatic type class|(}
   42.19 +\index{axiomatic type classes|(}
   42.20  \index{*axclass|(}
   42.21  
   42.22  
   42.23 @@ -62,7 +62,7 @@
   42.24  
   42.25  \input{Types/document/Axioms}
   42.26  
   42.27 -\index{axiomatic type class|)}
   42.28 +\index{axiomatic type classes|)}
   42.29  \index{*axclass|)}
   42.30  
   42.31  
    43.1 --- a/doc-src/TutorialI/basics.tex	Mon Jul 16 13:14:19 2001 +0200
    43.2 +++ b/doc-src/TutorialI/basics.tex	Tue Jul 17 13:46:21 2001 +0200
    43.3 @@ -42,8 +42,9 @@
    43.4  \section{Theories}
    43.5  \label{sec:Basic:Theories}
    43.6  
    43.7 +\index{theories|(}%
    43.8  Working with Isabelle means creating theories. Roughly speaking, a
    43.9 -\bfindex{theory} is a named collection of types, functions, and theorems,
   43.10 +\textbf{theory} is a named collection of types, functions, and theorems,
   43.11  much like a module in a programming language or a specification in a
   43.12  specification language. In fact, theories in HOL can be either. The general
   43.13  format of a theory \texttt{T} is
   43.14 @@ -61,7 +62,7 @@
   43.15  automatically visible. To avoid name clashes, identifiers can be
   43.16  \textbf{qualified} by theory names as in \texttt{T.f} and
   43.17  \texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
   43.18 -reside in a \bfindex{theory file} named \texttt{T.thy}.
   43.19 +reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.
   43.20  
   43.21  This tutorial is concerned with introducing you to the different linguistic
   43.22  constructs that can fill \textit{\texttt{declarations, definitions, and
   43.23 @@ -78,25 +79,25 @@
   43.24  proofs are in separate ML files.
   43.25  
   43.26  \begin{warn}
   43.27 -  HOL contains a theory \isaindexbold{Main}, the union of all the basic
   43.28 +  HOL contains a theory \thydx{Main}, the union of all the basic
   43.29    predefined theories like arithmetic, lists, sets, etc.  
   43.30    Unless you know what you are doing, always include \isa{Main}
   43.31    as a direct or indirect parent of all your theories.
   43.32 -\end{warn}
   43.33 +\end{warn}%
   43.34 +\index{theories|)}
   43.35  
   43.36  
   43.37  \section{Types, Terms and Formulae}
   43.38  \label{sec:TypesTermsForms}
   43.39 -\indexbold{type}
   43.40  
   43.41  Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
   43.42  logic whose type system resembles that of functional programming languages
   43.43 -like ML or Haskell. Thus there are
   43.44 +like ML or Haskell. Thus there are\index{types}
   43.45  \begin{description}
   43.46 -\item[base types,] in particular \isaindex{bool}, the type of truth values,
   43.47 -and \isaindex{nat}, the type of natural numbers.
   43.48 -\item[type constructors,] in particular \isaindex{list}, the type of
   43.49 -lists, and \isaindex{set}, the type of sets. Type constructors are written
   43.50 +\item[base types,] in particular \tydx{bool}, the type of truth values,
   43.51 +and \tydx{nat}, the type of natural numbers.
   43.52 +\item[type constructors,] in particular \tydx{list}, the type of
   43.53 +lists, and \tydx{set}, the type of sets. Type constructors are written
   43.54  postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
   43.55  natural numbers. Parentheses around single arguments can be dropped (as in
   43.56  \isa{nat list}), multiple arguments are separated by commas (as in
   43.57 @@ -108,7 +109,7 @@
   43.58    supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
   43.59    which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
   43.60      \isasymFun~$\tau$}.
   43.61 -\item[type variables,]\indexbold{type variable}\indexbold{variable!type}
   43.62 +\item[type variables,]\indexbold{type variables}\indexbold{variables!type}
   43.63    denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
   43.64    to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
   43.65    function.
   43.66 @@ -121,37 +122,37 @@
   43.67    the user, Isabelle infers the type of all variables automatically (this is
   43.68    called \bfindex{type inference}) and keeps quiet about it. Occasionally
   43.69    this may lead to misunderstandings between you and the system. If anything
   43.70 -  strange happens, we recommend to set the \rmindex{flag}
   43.71 -  \isaindexbold{show_types} that tells Isabelle to display type information
   43.72 -  that is usually suppressed: simply type
   43.73 +  strange happens, we recommend that you set the flag\index{flags}
   43.74 +  \isa{show_types}\index{*show_types (flag)}.  
   43.75 +  Isabelle will then display type information
   43.76 +  that is usually suppressed.   simply type
   43.77  \begin{ttbox}
   43.78  ML "set show_types"
   43.79  \end{ttbox}
   43.80  
   43.81  \noindent
   43.82  This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
   43.83 -which we introduce as we go along,
   43.84 -can be set and reset in the same manner.\indexbold{flag!(re)setting}
   43.85 +which we introduce as we go along, can be set and reset in the same manner.%
   43.86 +\index{flags!setting and resetting}
   43.87  \end{warn}
   43.88  
   43.89  
   43.90 -\textbf{Terms}\indexbold{term} are formed as in functional programming by
   43.91 +\textbf{Terms}\index{terms} are formed as in functional programming by
   43.92  applying functions to arguments. If \isa{f} is a function of type
   43.93  \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
   43.94  $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
   43.95  infix functions like \isa{+} and some basic constructs from functional
   43.96 -programming:
   43.97 +programming, such as conditional expressions:
   43.98  \begin{description}
   43.99 -\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
  43.100 -means what you think it means and requires that
  43.101 -$b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
  43.102 -\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}
  43.103 +\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if (symbol)}
  43.104 +Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
  43.105 +\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let (symbol)}
  43.106  is equivalent to $u$ where all occurrences of $x$ have been replaced by
  43.107  $t$. For example,
  43.108  \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
  43.109  by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
  43.110  \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
  43.111 -\indexbold{*case}
  43.112 +\indexbold{*case (symbol)}
  43.113  evaluates to $e@i$ if $e$ is of the form $c@i$.
  43.114  \end{description}
  43.115  
  43.116 @@ -162,8 +163,8 @@
  43.117  \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
  43.118  \isa{\isasymlambda{}x~y~z.~$t$}.
  43.119  
  43.120 -\textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.
  43.121 -There are the basic constants \isaindexbold{True} and \isaindexbold{False} and
  43.122 +\textbf{Formulae}\indexbold{formulae} are terms of type \tydx{bool}.
  43.123 +There are the basic constants \cdx{True} and \cdx{False} and
  43.124  the usual logical connectives (in decreasing order of priority):
  43.125  \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
  43.126  \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
  43.127 @@ -191,7 +192,7 @@
  43.128  \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
  43.129  
  43.130  Despite type inference, it is sometimes necessary to attach explicit
  43.131 -\textbf{type constraints}\indexbold{type constraint} to a term.  The syntax is
  43.132 +\bfindex{type constraints} to a term.  The syntax is
  43.133  \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
  43.134  \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
  43.135  in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
  43.136 @@ -208,8 +209,8 @@
  43.137  additional parentheses. In those cases where Isabelle echoes your
  43.138  input, you can see which parentheses are dropped --- they were superfluous. If
  43.139  you are unsure how to interpret Isabelle's output because you don't know
  43.140 -where the (dropped) parentheses go, set the \rmindex{flag}
  43.141 -\isaindexbold{show_brackets}:
  43.142 +where the (dropped) parentheses go, set the flag\index{flags}
  43.143 +\isa{show_brackets}\index{*show_brackets (flag)}:
  43.144  \begin{ttbox}
  43.145  ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
  43.146  \end{ttbox}
  43.147 @@ -232,8 +233,8 @@
  43.148  \item
  43.149  Constructs with an opening but without a closing delimiter bind very weakly
  43.150  and should therefore be enclosed in parentheses if they appear in subterms, as
  43.151 -in \isa{(\isasymlambda{}x.~x) = f}. This includes \isaindex{if},
  43.152 -\isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
  43.153 +in \isa{(\isasymlambda{}x.~x) = f}. This includes \sdx{if},
  43.154 +\sdx{let}, \sdx{case}, \isa{\isasymlambda}, and quantifiers.
  43.155  \item
  43.156  Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
  43.157  because \isa{x.x} is always read as a single qualified identifier that
  43.158 @@ -253,9 +254,10 @@
  43.159  
  43.160  Isabelle distinguishes free and bound variables just as is customary. Bound
  43.161  variables are automatically renamed to avoid clashes with free variables. In
  43.162 -addition, Isabelle has a third kind of variable, called a \bfindex{schematic
  43.163 -  variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
  43.164 -with a \isa{?}.  Logically, an unknown is a free variable. But it may be
  43.165 +addition, Isabelle has a third kind of variable, called a \textbf{schematic
  43.166 +  variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, 
  43.167 +which must a~\isa{?} as its first character.  
  43.168 +Logically, an unknown is a free variable. But it may be
  43.169  instantiated by another term during the proof process. For example, the
  43.170  mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
  43.171  which means that Isabelle can instantiate it arbitrarily. This is in contrast
    44.1 --- a/doc-src/TutorialI/fp.tex	Mon Jul 16 13:14:19 2001 +0200
    44.2 +++ b/doc-src/TutorialI/fp.tex	Tue Jul 17 13:46:21 2001 +0200
    44.3 @@ -126,8 +126,9 @@
    44.4    the files have not been modified).
    44.5    
    44.6    If you suddenly discover that you need to modify a parent theory of your
    44.7 -  current theory, you must first abandon your current theory\indexbold{abandon
    44.8 -  theory}\indexbold{theory!abandon} (at the shell
    44.9 +  current theory, you must first abandon your current theory%
   44.10 +  \indexbold{abandoning a theory}\indexbold{theories!abandoning} 
   44.11 +  (at the shell
   44.12    level type \commdx{kill}). After the parent theory has
   44.13    been modified, you go back to your original theory. When its first line
   44.14    \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
   44.15 @@ -154,12 +155,12 @@
   44.16  
   44.17  
   44.18  \subsection{Lists}
   44.19 -\indexbold{*list}
   44.20  
   44.21 +\index{*list (type)}%
   44.22  Lists are one of the essential datatypes in computing. Readers of this
   44.23  tutorial and users of HOL need to be familiar with their basic operations.
   44.24  Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
   44.25 -\isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
   44.26 +\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
   44.27  The latter contains many further operations. For example, the functions
   44.28  \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
   44.29  element and the remainder of a list. (However, pattern-matching is usually
   44.30 @@ -205,8 +206,8 @@
   44.31  \subsection{Primitive Recursion}
   44.32  
   44.33  Functions on datatypes are usually defined by recursion. In fact, most of the
   44.34 -time they are defined by what is called \bfindex{primitive recursion}.
   44.35 -The keyword \isacommand{primrec}\indexbold{*primrec} is followed by a list of
   44.36 +time they are defined by what is called \textbf{primitive recursion}.
   44.37 +The keyword \commdx{primrec} is followed by a list of
   44.38  equations
   44.39  \[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
   44.40  such that $C$ is a constructor of the datatype $t$ and all recursive calls of
   44.41 @@ -230,12 +231,12 @@
   44.42  
   44.43  \subsection{Natural Numbers}
   44.44  \label{sec:nat}
   44.45 -\index{arithmetic|(}
   44.46 +\index{linear arithmetic|(}
   44.47  
   44.48  \input{Misc/document/fakenat.tex}
   44.49  \input{Misc/document/natsum.tex}
   44.50  
   44.51 -\index{arithmetic|)}
   44.52 +\index{linear arithmetic|)}
   44.53  
   44.54  
   44.55  \subsection{Pairs}
   44.56 @@ -256,17 +257,18 @@
   44.57  
   44.58  
   44.59  \subsection{Type Synonyms}
   44.60 -\indexbold{type synonym}
   44.61  
   44.62 -Type synonyms are similar to those found in ML\@. Their syntax is fairly self
   44.63 -explanatory:
   44.64 +\indexbold{type synonyms|(}%
   44.65 +Type synonyms are similar to those found in ML\@. They are issued by a 
   44.66 +\commdx{types} command:
   44.67  
   44.68  \input{Misc/document/types.tex}%
   44.69  
   44.70  Note that pattern-matching is not allowed, i.e.\ each definition must be of
   44.71  the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
   44.72  Section~{\S}\ref{sec:Simp-with-Defs} explains how definitions are used
   44.73 -in proofs.
   44.74 +in proofs.%
   44.75 +\indexbold{type synonyms|)}
   44.76  
   44.77  \input{Misc/document/prime_def.tex}
   44.78  
   44.79 @@ -359,11 +361,14 @@
   44.80  
   44.81  \section{Advanced Datatypes}
   44.82  \label{sec:advanced-datatypes}
   44.83 -\index{*datatype|(}
   44.84 -\index{*primrec|(}
   44.85 +\index{datatype@\isacommand {datatype} (command)|(}
   44.86 +\index{primrec@\isacommand {primrec} (command)|(}
   44.87  %|)
   44.88  
   44.89 -This section presents advanced forms of \isacommand{datatype}s.
   44.90 +This section presents advanced forms of datatypes: mutual and nested
   44.91 +recursion.  A series of examples will culminate in a treatment of the trie
   44.92 +data structure.
   44.93 +
   44.94  
   44.95  \subsection{Mutual Recursion}
   44.96  \label{sec:datatype-mut-rec}
   44.97 @@ -412,9 +417,9 @@
   44.98  expressing the type of \emph{continuous} functions. 
   44.99  There is even a version of LCF on top of HOL,
  44.100  called HOLCF~\cite{MuellerNvOS99}.
  44.101 +\index{datatype@\isacommand {datatype} (command)|)}
  44.102 +\index{primrec@\isacommand {primrec} (command)|)}
  44.103  
  44.104 -\index{*primrec|)}
  44.105 -\index{*datatype|)}
  44.106  
  44.107  \subsection{Case Study: Tries}
  44.108  \label{sec:Trie}
  44.109 @@ -472,7 +477,7 @@
  44.110  
  44.111  \section{Total Recursive Functions}
  44.112  \label{sec:recdef}
  44.113 -\index{*recdef|(}
  44.114 +\index{recdef@\isacommand {recdef} (command)|(}\index{functions!total|(}
  44.115  
  44.116  Although many total functions have a natural primitive recursive definition,
  44.117  this is not always the case. Arbitrary total recursive functions can be
  44.118 @@ -504,4 +509,4 @@
  44.119  
  44.120  \index{induction!recursion|)}
  44.121  \index{recursion induction|)}
  44.122 -\index{*recdef|)}
  44.123 +\index{recdef@\isacommand {recdef} (command)|)}\index{functions!total|)}
    45.1 --- a/doc-src/TutorialI/tutorial.ind	Mon Jul 16 13:14:19 2001 +0200
    45.2 +++ b/doc-src/TutorialI/tutorial.ind	Tue Jul 17 13:46:21 2001 +0200
    45.3 @@ -86,8 +86,8 @@
    45.4  
    45.5    \indexspace
    45.6  
    45.7 -  \item abandon proof, \bold{11}
    45.8 -  \item abandon theory, \bold{14}
    45.9 +  \item abandoning a proof, \bold{11}
   45.10 +  \item abandoning a theory, \bold{14}
   45.11    \item \isa {abs} (constant), \hyperpage{135}
   45.12    \item \texttt {abs}, \bold{189}
   45.13    \item absolute value, \hyperpage{135}
   45.14 @@ -101,18 +101,16 @@
   45.15    \item \isacommand {apply} (command), \hyperpage{13}
   45.16    \item \isa {arg_cong} (theorem), \bold{80}
   45.17    \item \isa {arith} (method), \hyperpage{21}, \hyperpage{131}
   45.18 -  \item arithmetic, \hyperpage{20--21}, \hyperpage{31}
   45.19    \item \textsc {ascii} symbols, \bold{189}
   45.20    \item associative-commutative function, \hyperpage{158}
   45.21    \item \isa {assumption} (method), \hyperpage{53}
   45.22    \item assumptions
   45.23      \subitem renaming, \hyperpage{66--67}
   45.24      \subitem reusing, \hyperpage{67}
   45.25 -  \item \isa {auto}, \hyperpage{36}
   45.26 -  \item \isa {auto} (method), \hyperpage{76}
   45.27 +  \item \isa {auto} (method), \hyperpage{36}, \hyperpage{76}
   45.28    \item \isa {axclass}, \hyperpage{144--150}
   45.29    \item axiom of choice, \hyperpage{70}
   45.30 -  \item axiomatic type class, \hyperpage{144--150}
   45.31 +  \item axiomatic type classes, \hyperpage{144--150}
   45.32  
   45.33    \indexspace
   45.34  
   45.35 @@ -126,9 +124,9 @@
   45.36    \item \isa {bij_def} (theorem), \bold{94}
   45.37    \item bijections, \hyperpage{94}
   45.38    \item binomial coefficients, \hyperpage{93}
   45.39 -  \item bisimulation, \bold{100}
   45.40 +  \item bisimulations, \hyperpage{100}
   45.41    \item \isa {blast} (method), \hyperpage{72--75}
   45.42 -  \item \isa {bool}, \hyperpage{2}, \bold{3}
   45.43 +  \item \isa {bool} (type), \hyperpage{2, 3}
   45.44    \item \isa {bspec} (theorem), \bold{92}
   45.45    \item \isacommand{by} (command), \hyperpage{57}
   45.46  
   45.47 @@ -138,17 +136,14 @@
   45.48    \item \isa {card_Pow} (theorem), \bold{93}
   45.49    \item \isa {card_Un_Int} (theorem), \bold{93}
   45.50    \item cardinality, \hyperpage{93}
   45.51 -  \item \isa {case}, \bold{3}, \hyperpage{4}, \bold{16}, 
   45.52 +  \item \isa {case} (symbol), \bold{3}, \hyperpage{4}, \hyperpage{16}, 
   45.53  		\hyperpage{30, 31}
   45.54    \item case distinction, \bold{17}
   45.55    \item case splits, \bold{29}
   45.56 -  \item \isa {case_tac}, \bold{17}
   45.57 -  \item \isa {case_tac} (method), \hyperpage{85}
   45.58 +  \item \isa {case_tac} (method), \hyperpage{17}, \hyperpage{85}
   45.59    \item \isa {clarify} (method), \hyperpage{74}, \hyperpage{76}
   45.60    \item \isa {clarsimp} (method), \hyperpage{75, 76}
   45.61    \item \isa {classical} (theorem), \bold{57}
   45.62 -  \item closure
   45.63 -    \subitem reflexive and transitive, \hyperpage{96--98}
   45.64    \item coinduction, \bold{100}
   45.65    \item \isa {Collect} (constant), \hyperpage{93}
   45.66    \item \isa {comp_def} (theorem), \bold{96}
   45.67 @@ -161,8 +156,8 @@
   45.68    \item congruence rules, \bold{157}
   45.69    \item \isa {conjE} (theorem), \bold{55}
   45.70    \item \isa {conjI} (theorem), \bold{52}
   45.71 -  \item \isa {Cons}, \bold{7}
   45.72 -  \item \isa {constdefs}, \bold{23}
   45.73 +  \item \isa {Cons} (constant), \hyperpage{7}
   45.74 +  \item \isacommand {constdefs} (command), \hyperpage{23}
   45.75    \item contrapositives, \hyperpage{57}
   45.76    \item converse
   45.77      \subitem of a relation, \bold{96}
   45.78 @@ -171,11 +166,12 @@
   45.79  
   45.80    \indexspace
   45.81  
   45.82 -  \item \isa {datatype}, \hyperpage{7}, \hyperpage{36--42}
   45.83 +  \item \isacommand {datatype} (command), \hyperpage{7}, 
   45.84 +		\hyperpage{36--42}
   45.85    \item \isacommand {defer} (command), \hyperpage{14}, \hyperpage{84}
   45.86 -  \item definition, \bold{23}
   45.87 +  \item definitions, \bold{23}
   45.88      \subitem unfolding, \bold{28}
   45.89 -  \item \isa {defs}, \bold{23}
   45.90 +  \item \isacommand {defs} (command), \hyperpage{23}
   45.91    \item descriptions
   45.92      \subitem definite, \hyperpage{69}
   45.93      \subitem indefinite, \hyperpage{70}
   45.94 @@ -186,7 +182,7 @@
   45.95      \subitem of sets, \bold{90}
   45.96    \item \isa {disjCI} (theorem), \bold{58}
   45.97    \item \isa {disjE} (theorem), \bold{54}
   45.98 -  \item \isa {div}, \bold{20}
   45.99 +  \item \isa {div} (symbol), \hyperpage{20}
  45.100    \item divides relation, \hyperpage{68}, \hyperpage{78}, 
  45.101  		\hyperpage{85--87}, \hyperpage{134}
  45.102    \item division
  45.103 @@ -196,7 +192,7 @@
  45.104    \item domain
  45.105      \subitem of a relation, \hyperpage{96}
  45.106    \item \isa {Domain_iff} (theorem), \bold{96}
  45.107 -  \item done, \bold{11}
  45.108 +  \item \isacommand {done} (command), \hyperpage{11}
  45.109    \item \isa {drule_tac} (method), \hyperpage{60}, \hyperpage{80}
  45.110    \item \isa {dvd_add} (theorem), \bold{134}
  45.111    \item \isa {dvd_anti_sym} (theorem), \bold{134}
  45.112 @@ -209,10 +205,11 @@
  45.113    \item \isa {Eps} (constant), \hyperpage{93}
  45.114    \item equality
  45.115      \subitem of functions, \bold{93}
  45.116 +    \subitem of records, \hyperpage{143}
  45.117      \subitem of sets, \bold{90}
  45.118    \item \isa {equalityE} (theorem), \bold{90}
  45.119    \item \isa {equalityI} (theorem), \bold{90}
  45.120 -  \item \isa {erule}, \hyperpage{54}
  45.121 +  \item \isa {erule} (method), \hyperpage{54}
  45.122    \item \isa {erule_tac} (method), \hyperpage{60}
  45.123    \item Euclid's algorithm, \hyperpage{85--87}
  45.124    \item even numbers
  45.125 @@ -224,25 +221,28 @@
  45.126    \item \isa {ext} (theorem), \bold{93}
  45.127    \item extensionality
  45.128      \subitem for functions, \bold{93, 94}
  45.129 +    \subitem for records, \hyperpage{143}
  45.130      \subitem for sets, \bold{90}
  45.131    \item \ttEXU, \bold{189}
  45.132  
  45.133    \indexspace
  45.134  
  45.135 -  \item \isa {False}, \bold{3}
  45.136 +  \item \isa {False} (constant), \hyperpage{3}
  45.137    \item \isa {fast} (method), \hyperpage{75, 76}
  45.138    \item \isa {finite} (symbol), \hyperpage{93}
  45.139    \item \isa {Finites} (constant), \hyperpage{93}
  45.140    \item fixed points, \hyperpage{100}
  45.141 -  \item flag, \hyperpage{3, 4}, \hyperpage{31}
  45.142 -    \subitem (re)setting, \bold{3}
  45.143 +  \item flags, \hyperpage{3, 4}, \hyperpage{31}
  45.144 +    \subitem setting and resetting, \hyperpage{3}
  45.145    \item \isa {force} (method), \hyperpage{75, 76}
  45.146 -  \item formula, \bold{3}
  45.147 +  \item formulae, \bold{3}
  45.148    \item forward proof, \hyperpage{76--82}
  45.149    \item \isa {frule} (method), \hyperpage{67}
  45.150    \item \isa {frule_tac} (method), \hyperpage{60}
  45.151 -  \item \isa {fst}, \bold{21}
  45.152 +  \item \isa {fst} (constant), \hyperpage{21}
  45.153    \item functions, \hyperpage{93--95}
  45.154 +    \subitem total, \hyperpage{9}, \hyperpage{45--50}
  45.155 +    \subitem underdefined, \hyperpage{165}
  45.156  
  45.157    \indexspace
  45.158  
  45.159 @@ -256,7 +256,7 @@
  45.160    \item \isa {hd} (constant), \hyperpage{15}
  45.161    \item higher-order pattern, \bold{159}
  45.162    \item Hilbert's $\varepsilon$-operator, \hyperpage{69--71}
  45.163 -  \item {\textit {hypreal}} (type), \hyperpage{137}
  45.164 +  \item \isa {hypreal} (type), \hyperpage{137}
  45.165  
  45.166    \indexspace
  45.167  
  45.168 @@ -266,7 +266,7 @@
  45.169      \subitem qualified, \bold{2}
  45.170    \item identity function, \bold{94}
  45.171    \item identity relation, \bold{96}
  45.172 -  \item \isa {if}, \bold{3}, \hyperpage{4}
  45.173 +  \item \isa {if} (symbol), \bold{3}, \hyperpage{4}
  45.174    \item \isa {iff} (attribute), \hyperpage{73, 74}, \hyperpage{86}, 
  45.175  		\hyperpage{114}
  45.176    \item \isa {iffD1} (theorem), \bold{78}
  45.177 @@ -278,18 +278,19 @@
  45.178    \item \isa {Image_iff} (theorem), \bold{96}
  45.179    \item \isa {impI} (theorem), \bold{56}
  45.180    \item implication, \hyperpage{56--57}
  45.181 -  \item \isa {induct_tac}, \hyperpage{10}, \hyperpage{17}, 
  45.182 +  \item \isa {induct_tac} (method), \hyperpage{10}, \hyperpage{17}, 
  45.183  		\hyperpage{50}, \hyperpage{172}
  45.184    \item induction, \hyperpage{168--175}
  45.185      \subitem recursion, \hyperpage{49--50}
  45.186      \subitem structural, \bold{17}
  45.187      \subitem well-founded, \hyperpage{99}
  45.188    \item \isacommand {inductive} (command), \hyperpage{111}
  45.189 -  \item inductive definition, \hyperpage{111--129}
  45.190 +  \item inductive definition
  45.191      \subitem simultaneous, \hyperpage{125}
  45.192 +  \item inductive definitions, \hyperpage{111--129}
  45.193    \item \isacommand {inductive\_cases} (command), \hyperpage{115}, 
  45.194  		\hyperpage{123}
  45.195 -  \item \isa {infixr}, \bold{8}
  45.196 +  \item \isacommand{infixr} (annotation), \hyperpage{8}
  45.197    \item \isa {inj_on_def} (theorem), \bold{94}
  45.198    \item injections, \hyperpage{94}
  45.199    \item inner syntax, \bold{9}
  45.200 @@ -327,58 +328,62 @@
  45.201  
  45.202    \indexspace
  45.203  
  45.204 -  \item \isa {LEAST}, \bold{21}
  45.205 -  \item least number operator, \hyperpage{69}
  45.206 -  \item lemma, \hyperpage{11}
  45.207 -  \item \isa {lemma}, \bold{11}
  45.208 +  \item \isa {LEAST} (symbol), \hyperpage{21}, \hyperpage{69}
  45.209 +  \item least number operator, \see{\protect\isa{LEAST}}{69}
  45.210 +  \item \isacommand {lemma} (command), \hyperpage{11}
  45.211    \item \isacommand {lemmas} (command), \hyperpage{77}, \hyperpage{86}
  45.212    \item \isa {length} (symbol), \hyperpage{15}
  45.213    \item \isa {length_induct}, \bold{172}
  45.214    \item \isa {less_than} (constant), \hyperpage{98}
  45.215    \item \isa {less_than_iff} (theorem), \bold{98}
  45.216 -  \item \isa {let}, \bold{3}, \hyperpage{4}, \hyperpage{29}
  45.217 +  \item \isa {let} (symbol), \bold{3}, \hyperpage{4}, \hyperpage{29}
  45.218    \item \isa {lex_prod_def} (theorem), \bold{99}
  45.219    \item lexicographic product, \bold{99}, \hyperpage{160}
  45.220    \item {\texttt{lfp}}
  45.221      \subitem applications of, \see{CTL}{100}
  45.222 -  \item linear arithmetic, \bold{21}, \hyperpage{131}
  45.223 -  \item \isa {list}, \hyperpage{2}, \bold{7}, \bold{15}
  45.224 +  \item linear arithmetic, \hyperpage{20--21}, \hyperpage{31}, 
  45.225 +		\hyperpage{131}
  45.226 +  \item \isa {List} (theory), \hyperpage{15}
  45.227 +  \item \isa {list} (type), \hyperpage{2}, \hyperpage{7}, 
  45.228 +		\hyperpage{15}
  45.229    \item \isa {lists_mono} (theorem), \bold{121}
  45.230 +  \item Lowe, Gavin, \hyperpage{178--179}
  45.231  
  45.232    \indexspace
  45.233  
  45.234 -  \item \isa {Main}, \bold{2}
  45.235 +  \item \isa {Main} (theory), \hyperpage{2}
  45.236    \item major premise, \bold{59}
  45.237 -  \item \isa {max}, \bold{20, 21}
  45.238 +  \item \isa {max} (constant), \hyperpage{20, 21}
  45.239    \item measure function, \bold{45}, \bold{98}
  45.240    \item \isa {measure_def} (theorem), \bold{99}
  45.241    \item meta-logic, \bold{64}
  45.242    \item methods, \bold{14}
  45.243 -  \item \isa {min}, \bold{20, 21}
  45.244 -  \item \isa {mod}, \bold{20}
  45.245 +  \item \isa {min} (constant), \hyperpage{20, 21}
  45.246 +  \item \isa {mod} (symbol), \hyperpage{20}
  45.247    \item \isa {mod_div_equality} (theorem), \bold{133}
  45.248    \item \isa {mod_mult_distrib} (theorem), \bold{133}
  45.249    \item \emph{modus ponens}, \hyperpage{51}, \hyperpage{56}
  45.250    \item \isa {mono_def} (theorem), \bold{100}
  45.251    \item monotone functions, \bold{100}, \hyperpage{123}
  45.252      \subitem and inductive definitions, \hyperpage{121--122}
  45.253 +  \item \isa {more} (constant), \hyperpage{140--142}
  45.254    \item \isa {mp} (theorem), \bold{56}
  45.255    \item multiset ordering, \bold{99}
  45.256  
  45.257    \indexspace
  45.258  
  45.259 -  \item \isa {nat}, \hyperpage{2}
  45.260 -  \item \isa {nat} (type), \hyperpage{133--134}
  45.261 -  \item {\textit {nat}} (type), \hyperpage{20}
  45.262 +  \item \isa {nat} (type), \hyperpage{2}, \hyperpage{20}, 
  45.263 +		\hyperpage{133--134}
  45.264    \item natural deduction, \hyperpage{51--52}
  45.265    \item natural numbers, \hyperpage{133--134}
  45.266 +  \item Needham-Schroeder protocol, \hyperpage{177--179}
  45.267    \item negation, \hyperpage{57--59}
  45.268 -  \item \isa {Nil}, \bold{7}
  45.269 +  \item \isa {Nil} (constant), \hyperpage{7}
  45.270    \item \isa {no_asm}, \bold{27}
  45.271    \item \isa {no_asm_simp}, \bold{27}
  45.272    \item \isa {no_asm_use}, \bold{28}
  45.273    \item non-standard reals, \hyperpage{137}
  45.274 -  \item \isa {None}, \bold{22}
  45.275 +  \item \isa {None} (constant), \bold{22}
  45.276    \item \isa {notE} (theorem), \bold{57}
  45.277    \item \isa {notI} (theorem), \bold{57}
  45.278    \item numeric literals, \hyperpage{132}
  45.279 @@ -392,8 +397,8 @@
  45.280    \item \isa {o_def} (theorem), \bold{94}
  45.281    \item \isa {OF} (attribute), \hyperpage{78--79}
  45.282    \item \isa {of} (attribute), \hyperpage{77}, \hyperpage{79}
  45.283 -  \item \isa {oops}, \bold{11}
  45.284 -  \item \isa {option}, \bold{22}
  45.285 +  \item \isacommand {oops} (command), \hyperpage{11}
  45.286 +  \item \isa {option} (type), \bold{22}
  45.287    \item ordered rewriting, \bold{158}
  45.288    \item outer syntax, \bold{9}
  45.289    \item overloading, \hyperpage{144--146}
  45.290 @@ -401,7 +406,7 @@
  45.291  
  45.292    \indexspace
  45.293  
  45.294 -  \item pair, \bold{21}, \hyperpage{137--140}
  45.295 +  \item pairs and tuples, \hyperpage{21}, \hyperpage{137--140}
  45.296    \item parent theory, \bold{2}
  45.297    \item partial function, \hyperpage{164}
  45.298    \item pattern, higher-order, \bold{159}
  45.299 @@ -409,14 +414,16 @@
  45.300    \item permutative rewrite rule, \bold{158}
  45.301    \item \isacommand {pr} (command), \hyperpage{14}, \hyperpage{83}
  45.302    \item \isacommand {prefer} (command), \hyperpage{14}, \hyperpage{84}
  45.303 -  \item primitive recursion, \bold{16}
  45.304 -  \item \isa {primrec}, \hyperpage{8}, \bold{16}, \hyperpage{36--42}
  45.305 -  \item product type, \see{pair}{1}
  45.306 -  \item proof
  45.307 -    \subitem abandon, \bold{11}
  45.308 +  \item primitive recursion, \see{\isacommand{primrec}}{1}
  45.309 +  \item \isacommand {primrec} (command), \hyperpage{8}, \hyperpage{16}, 
  45.310 +		\hyperpage{36--42}
  45.311 +  \item product type, \see{pairs and tuples}{1}
  45.312    \item Proof General, \bold{5}
  45.313    \item proofs
  45.314 +    \subitem abandoning, \bold{11}
  45.315      \subitem examples of failing, \hyperpage{71--72}
  45.316 +  \item protocols
  45.317 +    \subitem security, \hyperpage{177--187}
  45.318  
  45.319    \indexspace
  45.320  
  45.321 @@ -436,28 +443,33 @@
  45.322      \subitem of a relation, \hyperpage{96}
  45.323    \item \isa {range} (symbol), \hyperpage{95}
  45.324    \item \isa {Range_iff} (theorem), \bold{96}
  45.325 +  \item \isa {Real} (theory), \hyperpage{137}
  45.326    \item \isa {real} (type), \hyperpage{136--137}
  45.327    \item real numbers, \hyperpage{136--137}
  45.328 -  \item \isa {recdef}, \hyperpage{45--50}, \hyperpage{160--168}
  45.329 -  \item \isacommand {recdef} (command), \hyperpage{98}
  45.330 -  \item \protect\isacommand{recdef} (command)
  45.331 +  \item \isacommand {recdef} (command), \hyperpage{45--50}, 
  45.332 +		\hyperpage{98}, \hyperpage{160--168}
  45.333      \subitem and numeric literals, \hyperpage{132}
  45.334 -  \item \isa {recdef_cong}, \bold{164}
  45.335 +  \item \isa {recdef_cong} (attribute), \hyperpage{164}
  45.336    \item \isa {recdef_simp}, \bold{47}
  45.337    \item \isa {recdef_wf}, \bold{162}
  45.338 +  \item \isacommand {record} (command), \hyperpage{140}
  45.339 +  \item \isa {record_split} (method), \hyperpage{143}
  45.340 +  \item records, \hyperpage{140--144}
  45.341 +    \subitem extensible, \hyperpage{141--142}
  45.342    \item recursion
  45.343      \subitem well-founded, \bold{161}
  45.344    \item recursion induction, \hyperpage{49--50}
  45.345    \item \isacommand {redo} (command), \hyperpage{14}
  45.346 +  \item reflexive and transitive closure, \hyperpage{96--98}
  45.347    \item relations, \hyperpage{95--98}
  45.348      \subitem well-founded, \hyperpage{98--99}
  45.349    \item \isa {rename_tac} (method), \hyperpage{66--67}
  45.350 -  \item \isa {rev}, \bold{8}
  45.351 +  \item \isa {rev} (constant), \hyperpage{8}
  45.352    \item rewrite rule, \bold{26}
  45.353      \subitem permutative, \bold{158}
  45.354    \item rewriting, \bold{26}
  45.355      \subitem ordered, \bold{158}
  45.356 -  \item \isa {rotate_tac}, \bold{28}
  45.357 +  \item \isa {rotate_tac} (method), \hyperpage{28}
  45.358    \item \isa {rtrancl_refl} (theorem), \bold{96}
  45.359    \item \isa {rtrancl_trans} (theorem), \bold{96}
  45.360    \item rule induction, \hyperpage{112--114}
  45.361 @@ -469,20 +481,19 @@
  45.362  
  45.363    \item \isa {safe} (method), \hyperpage{75, 76}
  45.364    \item safe rules, \bold{73}
  45.365 -  \item schematic variable, \bold{4}
  45.366 -  \item \isa {set}, \hyperpage{2}
  45.367 -  \item {\textit {set}} (type), \hyperpage{89}
  45.368 +  \item \isa {set} (type), \hyperpage{2}, \hyperpage{89}
  45.369    \item set comprehensions, \hyperpage{91--92}
  45.370    \item \isa {set_ext} (theorem), \bold{90}
  45.371    \item sets, \hyperpage{89--93}
  45.372      \subitem finite, \hyperpage{93}
  45.373      \subitem notation for finite, \bold{91}
  45.374 -  \item \isa {show_brackets}, \bold{4}
  45.375 -  \item \isa {show_types}, \bold{3}
  45.376 +  \item settings, \see{flags}{1}
  45.377 +  \item \isa {show_brackets} (flag), \hyperpage{4}
  45.378 +  \item \isa {show_types} (flag), \hyperpage{3}
  45.379    \item \texttt {show_types}, \hyperpage{14}
  45.380    \item \isa {simp} (attribute), \bold{9}, \hyperpage{26}
  45.381    \item \isa {simp} (method), \bold{26}
  45.382 -  \item \isa {simp_all}, \hyperpage{26}, \hyperpage{36}
  45.383 +  \item \isa {simp_all} (method), \hyperpage{26}, \hyperpage{36}
  45.384    \item simplification, \hyperpage{25--32}, \hyperpage{157--160}
  45.385      \subitem of let-expressions, \hyperpage{29}
  45.386      \subitem ordered, \bold{158}
  45.387 @@ -492,20 +503,20 @@
  45.388    \item \isa {simplified} (attribute), \hyperpage{77}, \hyperpage{79}
  45.389    \item simplifier, \bold{25}
  45.390    \item \isa {size} (constant), \hyperpage{15}
  45.391 -  \item \isa {snd}, \bold{21}
  45.392 +  \item \isa {snd} (constant), \hyperpage{21}
  45.393    \item \isa {SOME} (symbol), \hyperpage{69}
  45.394    \item \texttt {SOME}, \bold{189}
  45.395 -  \item \isa {Some}, \bold{22}
  45.396 +  \item \isa {Some} (constant), \bold{22}
  45.397    \item \isa {some_equality} (theorem), \bold{69}
  45.398    \item \isa {someI} (theorem), \bold{70}
  45.399    \item \isa {someI2} (theorem), \bold{70}
  45.400    \item \isa {someI_ex} (theorem), \bold{71}
  45.401 -  \item sort, \bold{150}
  45.402 +  \item sorts, \hyperpage{150}
  45.403    \item \isa {spec} (theorem), \bold{64}
  45.404    \item \isa {split} (constant), \bold{137}
  45.405    \item \isa {split} (method, attr.), \hyperpage{29--31}
  45.406    \item split rule, \bold{30}
  45.407 -  \item \isa {split_if}, \bold{30}
  45.408 +  \item \isa {split_if} (theorem), \hyperpage{30}
  45.409    \item \isa {ssubst} (theorem), \bold{61}
  45.410    \item structural induction, \bold{17}
  45.411    \item \isa {subgoal_tac} (method), \hyperpage{81, 82}
  45.412 @@ -518,43 +529,40 @@
  45.413    \item \isa {surj_def} (theorem), \bold{94}
  45.414    \item surjections, \hyperpage{94}
  45.415    \item \isa {sym} (theorem), \bold{77}
  45.416 -  \item syntax translation, \bold{23}
  45.417 +  \item syntax translations, \hyperpage{23--24}
  45.418  
  45.419    \indexspace
  45.420  
  45.421 -  \item tactic, \bold{10}
  45.422    \item tacticals, \hyperpage{82--83}
  45.423 -  \item term, \bold{3}
  45.424 +  \item tactics, \hyperpage{10}
  45.425    \item \isacommand {term} (command), \hyperpage{14}
  45.426    \item term rewriting, \bold{26}
  45.427 -  \item termination, \see{total function}{1}
  45.428 +  \item termination, \see{functions, total}{1}
  45.429 +  \item terms, \hyperpage{3}
  45.430    \item \isa {THEN} (attribute), \bold{77}, \hyperpage{79}, 
  45.431  		\hyperpage{86}
  45.432 -  \item theorem, \hyperpage{11}
  45.433 -  \item \isa {theorem}, \bold{9}, \hyperpage{11}
  45.434 -  \item theory, \bold{2}
  45.435 -    \subitem abandon, \bold{14}
  45.436 -  \item theory file, \bold{2}
  45.437 +  \item \isacommand {theorem} (command), \bold{9}, \hyperpage{11}
  45.438 +  \item theories, \hyperpage{2}
  45.439 +    \subitem abandoning, \bold{14}
  45.440 +  \item theory files, \hyperpage{2}
  45.441    \item \isacommand {thm} (command), \hyperpage{14}
  45.442    \item \isa {tl} (constant), \hyperpage{15}
  45.443 -  \item total function, \hyperpage{9}
  45.444 -  \item \isa {trace_simp}, \bold{31}
  45.445 +  \item \isa {trace_simp} (flag), \hyperpage{31}
  45.446    \item tracing the simplifier, \bold{31}
  45.447    \item \isa {trancl_trans} (theorem), \bold{97}
  45.448 -  \item \isa {translations}, \bold{24}
  45.449 -  \item \isa {True}, \bold{3}
  45.450 -  \item tuple, \see{pair}{1}
  45.451 +  \item \isa {True} (constant), \hyperpage{3}
  45.452 +  \item tuples, \see{pairs and tuples}{1}
  45.453    \item \isacommand {typ} (command), \hyperpage{14}
  45.454 -  \item type, \bold{2}
  45.455 -  \item type constraint, \bold{4}
  45.456 -  \item type declaration, \bold{150}
  45.457 -  \item type definition, \bold{151}
  45.458 +  \item type constraints, \bold{4}
  45.459    \item type inference, \bold{3}
  45.460 -  \item type synonym, \bold{22}
  45.461 -  \item type variable, \bold{3}
  45.462 -  \item \isa {typedecl}, \bold{151}
  45.463 -  \item \isa {typedef}, \bold{151}
  45.464 -  \item \isa {types}, \bold{23}
  45.465 +  \item type synonyms, \hyperpage{22--23}
  45.466 +  \item type variables, \bold{3}
  45.467 +  \item \isacommand {typedecl} (command), \hyperpage{150}
  45.468 +  \item \isacommand {typedef} (command), \hyperpage{151--155}
  45.469 +  \item types, \hyperpage{2}
  45.470 +    \subitem declaring, \hyperpage{150--151}
  45.471 +    \subitem defining, \hyperpage{151--155}
  45.472 +  \item \isacommand {types} (command), \hyperpage{22}
  45.473  
  45.474    \indexspace
  45.475  
  45.476 @@ -564,31 +572,30 @@
  45.477    \item \isa {UN_I} (theorem), \bold{92}
  45.478    \item \isa {UN_iff} (theorem), \bold{92}
  45.479    \item \isa {Un_subset_iff} (theorem), \bold{90}
  45.480 -  \item underdefined function, \hyperpage{165}
  45.481    \item \isacommand {undo} (command), \hyperpage{14}
  45.482 -  \item \isa {unfold}, \bold{28}
  45.483    \item unification, \hyperpage{60--63}
  45.484    \item \isa {UNION} (constant), \hyperpage{93}
  45.485    \item \texttt {Union}, \bold{189}
  45.486    \item union
  45.487      \subitem indexed, \hyperpage{92}
  45.488    \item \isa {Union_iff} (theorem), \bold{92}
  45.489 -  \item \isa {unit}, \bold{22}
  45.490 -  \item unknown, \bold{4}
  45.491 -  \item unknowns, \bold{52}
  45.492 +  \item \isa {unit} (type), \hyperpage{22}
  45.493 +  \item unknowns, \hyperpage{4}, \bold{52}
  45.494    \item unsafe rules, \bold{73}
  45.495    \item updating a function, \bold{93}
  45.496  
  45.497    \indexspace
  45.498  
  45.499    \item variable, \bold{4}
  45.500 -    \subitem schematic, \bold{4}
  45.501 +  \item variables
  45.502 +    \subitem schematic, \hyperpage{4}
  45.503      \subitem type, \bold{3}
  45.504    \item \isa {vimage_def} (theorem), \bold{95}
  45.505  
  45.506    \indexspace
  45.507  
  45.508    \item \isa {wf_induct} (theorem), \bold{99}
  45.509 -  \item \isa {while}, \bold{167}
  45.510 +  \item \isa {while} (constant), \hyperpage{167}
  45.511 +  \item \isa {While_Combinator} (theory), \hyperpage{167}
  45.512  
  45.513  \end{theindex}
    46.1 --- a/doc-src/TutorialI/tutorial.sty	Mon Jul 16 13:14:19 2001 +0200
    46.2 +++ b/doc-src/TutorialI/tutorial.sty	Tue Jul 17 13:46:21 2001 +0200
    46.3 @@ -33,7 +33,7 @@
    46.4  \newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)|bold}}
    46.5  
    46.6  \newcommand\cldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (class)}}
    46.7 -\newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} (type)}}
    46.8 +\newcommand\tydx[1]{\textit{#1}\index{#1@\protect\isa{#1} (type)}}
    46.9  \newcommand\thydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theory)}}
   46.10  
   46.11  \newcommand\attrdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (attribute)}}
   46.12 @@ -52,8 +52,6 @@
   46.13  
   46.14  \newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
   46.15  \newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
   46.16 -\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}\@}
   46.17 -\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}\@}
   46.18  
   46.19  %\newtheorem{theorem}{Theorem}[section]
   46.20  \newtheorem{Exercise}{Exercise}[section]
    47.1 --- a/doc-src/TutorialI/tutorial.tex	Mon Jul 16 13:14:19 2001 +0200
    47.2 +++ b/doc-src/TutorialI/tutorial.tex	Tue Jul 17 13:46:21 2001 +0200
    47.3 @@ -10,9 +10,11 @@
    47.4  
    47.5  \makeindex
    47.6  
    47.7 -\index{termination|see{total function}}
    47.8 -\index{product type|see{pair}}
    47.9 -\index{tuple|see{pair}}
   47.10 +\index{primitive recursion|see{\isacommand{primrec}}}
   47.11 +\index{product type|see{pairs and tuples}}
   47.12 +\index{termination|see{functions, total}}
   47.13 +\index{tuples|see{pairs and tuples}}
   47.14 +\index{settings|see{flags}}
   47.15  \index{*<*lex*>|see{lexicographic product}}
   47.16  
   47.17  \underscoreoff