--- a/doc-src/TutorialI/Advanced/Partial.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy Tue Jul 17 13:46:21 2001 +0200
@@ -14,7 +14,7 @@
function was applied to an argument in its domain or not. If you do
not need to make this distinction, for example because the function is
never used outside its domain, it is easier to work with
-\emph{underdefined}\index{underdefined function} functions: for
+\emph{underdefined}\index{functions!underdefined} functions: for
certain arguments we only know that a result exists, but we do not
know what it is. When defining functions that are normally considered
partial, underdefinedness turns out to be a very reasonable
@@ -143,9 +143,9 @@
subsubsection{*The {\tt\slshape while} Combinator*}
text{*If the recursive function happens to be tail recursive, its
-definition becomes a triviality if based on the predefined \isaindexbold{while}
+definition becomes a triviality if based on the predefined \cdx{while}
combinator. The latter lives in the Library theory
-\isa{While_Combinator}, which is not part of @{text Main} but needs to
+\thydx{While_Combinator}, which is not part of @{text Main} but needs to
be included explicitly among the ancestor theories.
Constant @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}
--- a/doc-src/TutorialI/Advanced/advanced.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Advanced/advanced.tex Tue Jul 17 13:46:21 2001 +0200
@@ -10,7 +10,7 @@
\input{Advanced/document/simp.tex}
\section{Advanced Forms of Recursion}
-\index{*recdef|(}
+\index{recdef@\isacommand {recdef} (command)|(}
The purpose of this section is to introduce advanced forms of
\isacommand{recdef}: how to establish termination by means other than measure
@@ -41,7 +41,7 @@
\index{partial function}
\input{Advanced/document/Partial.tex}
-\index{*recdef|)}
+\index{recdef@\isacommand {recdef} (command)|)}
\section{Advanced Induction Techniques}
\label{sec:advanced-ind}
--- a/doc-src/TutorialI/Advanced/document/Partial.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Tue Jul 17 13:46:21 2001 +0200
@@ -17,7 +17,7 @@
function was applied to an argument in its domain or not. If you do
not need to make this distinction, for example because the function is
never used outside its domain, it is easier to work with
-\emph{underdefined}\index{underdefined function} functions: for
+\emph{underdefined}\index{functions!underdefined} functions: for
certain arguments we only know that a result exists, but we do not
know what it is. When defining functions that are normally considered
partial, underdefinedness turns out to be a very reasonable
@@ -149,9 +149,9 @@
%
\begin{isamarkuptext}%
If the recursive function happens to be tail recursive, its
-definition becomes a triviality if based on the predefined \isaindexbold{while}
+definition becomes a triviality if based on the predefined \cdx{while}
combinator. The latter lives in the Library theory
-\isa{While_Combinator}, which is not part of \isa{Main} but needs to
+\thydx{While_Combinator}, which is not part of \isa{Main} but needs to
be included explicitly among the ancestor theories.
Constant \isa{while} is of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Tue Jul 17 13:46:21 2001 +0200
@@ -110,8 +110,8 @@
apply(induct_tac xs, simp, simp split: instr.split);
(*<*)done(*>*)
text{*\noindent
-Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
-be modified in the same way @{text simp} can. Thus the proof can be
+Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
+be modified in the same way as @{text simp}. Thus the proof can be
rewritten as
*}
(*<*)
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Jul 17 13:46:21 2001 +0200
@@ -102,8 +102,8 @@
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
-be modified in the same way \isa{simp} can. Thus the proof can be
+Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
+be modified in the same way as \isa{simp}. Thus the proof can be
rewritten as%
\end{isamarkuptext}%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
--- a/doc-src/TutorialI/Inductive/inductive.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Inductive/inductive.tex Tue Jul 17 13:46:21 2001 +0200
@@ -1,5 +1,5 @@
\chapter{Inductively Defined Sets} \label{chap:inductive}
-\index{inductive definition|(}
+\index{inductive definitions|(}
This chapter is dedicated to the most important definition principle after
recursive functions and datatypes: inductively defined sets.
@@ -23,4 +23,4 @@
\input{Inductive/document/AB}
-\index{inductive definition|)}
+\index{inductive definitions|)}
--- a/doc-src/TutorialI/IsaMakefile Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile Tue Jul 17 13:46:21 2001 +0200
@@ -186,4 +186,4 @@
## clean
clean:
- @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
+ @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
--- a/doc-src/TutorialI/Makefile Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Makefile Tue Jul 17 13:46:21 2001 +0200
@@ -15,6 +15,13 @@
NAME = tutorial
FILES = tutorial.tex basics.tex fp.tex appendix.tex \
+ Advanced/advanced.tex \
+ CTL/ctl.tex \
+ Inductive/inductive.tex Inductive/even-example.tex \
+ Inductive/advanced-examples.tex \
+ Protocol/protocol.tex \
+ Rules/rules.tex Sets/sets.tex \
+ Types/numerics.tex Types/records.tex Types/types.tex \
../iman.sty ../ttbox.sty ../extra.sty \
isabelle.sty isabellesym.sty ../pdfsetup.sty
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Jul 17 13:46:21 2001 +0200
@@ -230,12 +230,12 @@
identity function.
\end{exercise}
-Method @{text induct_tac} can be applied with any rule $r$
+Method \methdx{induct_tac} can be applied with any rule $r$
whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
format is
\begin{quote}
\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
-\end{quote}\index{*induct_tac}%
+\end{quote}
where $y@1, \dots, y@n$ are variables in the first subgoal.
The conclusion of $r$ can even be an (iterated) conjunction of formulae of
the above form in which case the application is
--- a/doc-src/TutorialI/Misc/Option2.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy Tue Jul 17 13:46:21 2001 +0200
@@ -4,7 +4,8 @@
hide type option
(*>*)
-text{*\indexbold{*option}\indexbold{*None}\indexbold{*Some}
+text{*\indexbold{*option (type)}\indexbold{*None (constant)}%
+\indexbold{*Some (constant)}
Our final datatype is very simple but still eminently useful:
*}
--- a/doc-src/TutorialI/Misc/Translations.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/Translations.thy Tue Jul 17 13:46:21 2001 +0200
@@ -4,8 +4,10 @@
subsection{*Syntax Translations*}
text{*\label{sec:def-translations}
+\indexbold{syntax translations|(}%
+\indexbold{translations@\isacommand {translations} (command)|(}
Isabelle offers an additional definition-like facility,
-\textbf{syntax translations}\indexbold{syntax translation}.
+\textbf{syntax translations}.
They resemble macros: upon parsing, the defined concept is immediately
replaced by its definition, and this is reversed upon printing. For example,
the symbol @{text"\<noteq>"} is defined via a syntax translation:
@@ -13,7 +15,7 @@
translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
-text{*\indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
+text{*\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
\noindent
Internally, @{text"\<noteq>"} never appears.
@@ -27,7 +29,9 @@
via translations. Translations are preferable to definitions when the new
concept is a trivial variation on an existing one. For example, we
don't need to derive new theorems about @{text"\<noteq>"}, since existing theorems
-about @{text"="} still apply.
+about @{text"="} still apply.%
+\indexbold{syntax translations|)}%
+\indexbold{translations@\isacommand {translations} (command)|)}
*}
(*<*)
--- a/doc-src/TutorialI/Misc/case_exprs.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy Tue Jul 17 13:46:21 2001 +0200
@@ -5,7 +5,7 @@
subsection{*Case Expressions*}
text{*\label{sec:case-expressions}
-HOL also features \isaindexbold{case}-expressions for analyzing
+HOL also features \sdx{case}-expressions for analyzing
elements of a datatype. For example,
@{term[display]"case xs of [] => 1 | y#ys => y"}
evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if
@@ -47,10 +47,10 @@
\indexbold{induction!structural}
\indexbold{case distinction}
Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \isaindex{induct_tac},
+simplification. Only induction is invoked by hand via \methdx{induct_tac},
which works for any datatype. In some cases, induction is overkill and a case
distinction over all constructors of the datatype suffices. This is performed
-by \isaindexbold{case_tac}. A trivial example:
+by \methdx{case_tac}. A trivial example:
*}
lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Jul 17 13:46:21 2001 +0200
@@ -225,12 +225,12 @@
identity function.
\end{exercise}
-Method \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$
+Method \methdx{induct_tac} can be applied with any rule $r$
whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
format is
\begin{quote}
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
-\end{quote}\index{*induct_tac}%
+\end{quote}
where $y@1, \dots, y@n$ are variables in the first subgoal.
The conclusion of $r$ can even be an (iterated) conjunction of formulae of
the above form in which case the application is
--- a/doc-src/TutorialI/Misc/document/Option2.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Option2.tex Tue Jul 17 13:46:21 2001 +0200
@@ -3,7 +3,8 @@
\def\isabellecontext{Option{\isadigit{2}}}%
%
\begin{isamarkuptext}%
-\indexbold{*option}\indexbold{*None}\indexbold{*Some}
+\indexbold{*option (type)}\indexbold{*None (constant)}%
+\indexbold{*Some (constant)}
Our final datatype is very simple but still eminently useful:%
\end{isamarkuptext}%
\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a%
--- a/doc-src/TutorialI/Misc/document/Translations.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Translations.tex Tue Jul 17 13:46:21 2001 +0200
@@ -7,15 +7,17 @@
%
\begin{isamarkuptext}%
\label{sec:def-translations}
+\indexbold{syntax translations|(}%
+\indexbold{translations@\isacommand {translations} (command)|(}
Isabelle offers an additional definition-like facility,
-\textbf{syntax translations}\indexbold{syntax translation}.
+\textbf{syntax translations}.
They resemble macros: upon parsing, the defined concept is immediately
replaced by its definition, and this is reversed upon printing. For example,
the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
\end{isamarkuptext}%
\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
-\indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
+\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
\noindent
Internally, \isa{{\isasymnoteq}} never appears.
@@ -30,6 +32,8 @@
concept is a trivial variation on an existing one. For example, we
don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
about \isa{{\isacharequal}} still apply.%
+\indexbold{syntax translations|)}%
+\indexbold{translations@\isacommand {translations} (command)|)}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Tue Jul 17 13:46:21 2001 +0200
@@ -7,7 +7,7 @@
%
\begin{isamarkuptext}%
\label{sec:case-expressions}
-HOL also features \isaindexbold{case}-expressions for analyzing
+HOL also features \sdx{case}-expressions for analyzing
elements of a datatype. For example,
\begin{isabelle}%
\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
@@ -58,10 +58,10 @@
\indexbold{induction!structural}
\indexbold{case distinction}
Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \isaindex{induct_tac},
+simplification. Only induction is invoked by hand via \methdx{induct_tac},
which works for any datatype. In some cases, induction is overkill and a case
distinction over all constructors of the datatype suffices. This is performed
-by \isaindexbold{case_tac}. A trivial example:%
+by \methdx{case_tac}. A trivial example:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Jul 17 13:46:21 2001 +0200
@@ -26,13 +26,13 @@
}
The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
-\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
-\isaindexbold{max} are predefined, as are the relations
+\sdx{div}, \sdx{mod}, \cdx{min} and
+\cdx{max} are predefined, as are the relations
\indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
\isa{m\ {\isacharless}\ n}. There is even a least number operation
-\isaindexbold{LEAST}. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
-Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}}
+\sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
+Isabelle does not prove this automatically. Note that \isa{{\isadigit{1}}}
and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
\isa{Suc}-expressions. If you need the full set of numerals,
see~\S\ref{sec:numerals}.
@@ -40,8 +40,8 @@
\begin{warn}
The constant \cdx{0} and the operations
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
- \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
- \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
+ \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
+ \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
not just for natural numbers but at other types as well.
For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
@@ -76,7 +76,7 @@
\isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
and the operations
\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
-known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
+known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
For example,%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
@@ -93,8 +93,8 @@
\begin{warn}
The running time of \isa{arith} is exponential in the number of occurrences
- of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
- \isaindexbold{max} because they are first eliminated by case distinctions.
+ of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
+ \cdx{max} because they are first eliminated by case distinctions.
\isa{arith} is incomplete even for the restricted class of
linear arithmetic formulae. If divisibility plays a
--- a/doc-src/TutorialI/Misc/document/pairs.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Tue Jul 17 13:46:21 2001 +0200
@@ -3,11 +3,11 @@
\def\isabellecontext{pairs}%
%
\begin{isamarkuptext}%
-\label{sec:pairs}\indexbold{pair}
-HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
+\label{sec:pairs}\index{pairs and tuples}
+HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
-$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
-\isaindexbold{snd}:
+$\tau@i$. The functions \cdx{fst} and
+\cdx{snd} extract the components of a pair:
\isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
@@ -17,7 +17,7 @@
Remarks:
\begin{itemize}
\item
-There is also the type \isaindexbold{unit}, which contains exactly one
+There is also the type \tydx{unit}, which contains exactly one
element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
as a degenerate product with 0 components.
\item
--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Tue Jul 17 13:46:21 2001 +0200
@@ -57,7 +57,7 @@
proofs seen so far could have been performed
with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
only the first subgoal and may thus need to be repeated --- use
-\isaindex{simp_all} to simplify all subgoals.
+\methdx{simp_all} to simplify all subgoals.
Note that \isa{simp} fails if nothing changes.%
\end{isamarkuptext}%
%
@@ -138,7 +138,7 @@
Assumptions are simplified in a left-to-right fashion. If an
assumption can help in simplifying one to the left of it, this may get
overlooked. In such cases you have to rotate the assumptions explicitly:
-\isacommand{apply}\isa{{\isacharparenleft}rotate{\isacharunderscore}tac}~$n$\isa{{\isacharparenright}}\indexbold{*rotate_tac}
+\isacommand{apply}\isa{{\isacharparenleft}}\methdx{rotate_tac}~$n$\isa{{\isacharparenright}}
causes a cyclic shift by $n$ positions from right to left, if $n$ is
positive, and from left to right, if $n$ is negative.
Beware that such rotations make proofs quite brittle.
@@ -167,8 +167,8 @@
\isacommand{lemma}\ {\isachardoublequote}xor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
-get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
+Typically, we begin by unfolding some definitions:
+\indexbold{definitions!unfolding}%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptxt}%
@@ -200,7 +200,7 @@
%
\begin{isamarkuptext}%
\index{simplification!of let-expressions}
-Proving a goal containing \isaindex{let}-expressions almost invariably
+Proving a goal containing \sdx{let}-expressions almost invariably
requires the \isa{let}-con\-structs to be expanded at some point. Since
\isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for a predefined constant
(called \isa{Let}), expanding \isa{let}-constructs means rewriting with
@@ -262,13 +262,13 @@
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymforall}xs{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}%
\end{isabelle}
-where \isaindexbold{split_if} is a theorem that expresses splitting of
+where \tdx{split_if} is a theorem that expresses splitting of
\isa{if}s. Because
case-splitting on \isa{if}s is almost always the right proof strategy, the
simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
on the initial goal above.
-This splitting idea generalizes from \isa{if} to \isaindex{case}.
+This splitting idea generalizes from \isa{if} to \sdx{case}.
Let us simplify a case analysis over lists:%
\end{isamarkuptxt}%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
@@ -334,7 +334,7 @@
The simplifier merely simplifies the condition of an \isa{if} but not the
\isa{then} or \isa{else} parts. The latter are simplified only after the
condition reduces to \isa{True} or \isa{False}, or after splitting. The
- same is true for \isaindex{case}-expressions: only the selector is
+ same is true for \sdx{case}-expressions: only the selector is
simplified at first, until either the expression reduces to one of the
cases or it is split.
\end{warn}\index{*split (method, attr.)|)}%
@@ -344,7 +344,7 @@
}
%
\begin{isamarkuptext}%
-\index{arithmetic}
+\index{linear arithmetic}
The simplifier routinely solves a small class of linear arithmetic formulae
(over type \isa{nat} and other numeric types): it only takes into account
assumptions and conclusions that are relations
@@ -367,7 +367,8 @@
\begin{isamarkuptext}%
\indexbold{tracing the simplifier}
Using the simplifier effectively may take a bit of experimentation. Set the
-\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
+\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags}
+to get a better idea of what is going
on:%
\end{isamarkuptext}%
\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Misc/document/types.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex Tue Jul 17 13:46:21 2001 +0200
@@ -5,7 +5,7 @@
\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
\begin{isamarkuptext}%
-\noindent\indexbold{*types}%
+\noindent
Internally all synonyms are fully expanded. As a consequence Isabelle's
output never contains synonyms. Their main purpose is to improve the
readability of theories. Synonyms can be used just like any other
@@ -17,7 +17,7 @@
}
%
\begin{isamarkuptext}%
-\label{sec:ConstDefinitions}\indexbold{definition}%
+\label{sec:ConstDefinitions}\indexbold{definitions}%
The above constants \isa{nand} and \isa{xor} are non-recursive and can
therefore be defined directly by%
\end{isamarkuptext}%
@@ -25,19 +25,20 @@
\ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent%
-where \isacommand{defs}\indexbold{*defs} is a keyword and
+where \commdx{defs} is a keyword and
\isa{nand{\isacharunderscore}def} and \isa{xor{\isacharunderscore}def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
-Declarations and definitions can also be merged%
+Declarations and definitions can also be merged in a \commdx{constdefs}
+command:%
\end{isamarkuptext}%
\isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
\ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
\ \ \ \ \ \ \ \ \ \ xor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
\ \ \ \ \ \ \ \ \ {\isachardoublequote}xor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
-\noindent\indexbold{*constdefs}%
-in which case the default name of each definition is $f$\isa{{\isacharunderscore}def}, where
+\noindent
+The default name of each definition is $f$\isa{{\isacharunderscore}def}, where
$f$ is the name of the defined constant.%
\end{isamarkuptext}%
\end{isabellebody}%
--- a/doc-src/TutorialI/Misc/natsum.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Tue Jul 17 13:46:21 2001 +0200
@@ -24,13 +24,13 @@
}
The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
-\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
-\isaindexbold{max} are predefined, as are the relations
+\sdx{div}, \sdx{mod}, \cdx{min} and
+\cdx{max} are predefined, as are the relations
\indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if
@{prop"m<n"}. There is even a least number operation
-\isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although
-Isabelle does not prove this completely automatically. Note that @{term 1}
+\sdx{LEAST}\@. For example, @{prop"(LEAST n. 1 < n) = 2"}, although
+Isabelle does not prove this automatically. Note that @{term 1}
and @{term 2} are available as abbreviations for the corresponding
@{term Suc}-expressions. If you need the full set of numerals,
see~\S\ref{sec:numerals}.
@@ -38,8 +38,8 @@
\begin{warn}
The constant \cdx{0} and the operations
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
- \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min},
- \isaindexbold{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
+ \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
+ \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
not just for natural numbers but at other types as well.
For example, given the goal @{prop"x+0 = x"},
@@ -76,7 +76,7 @@
@{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
and the operations
@{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
-known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
+known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
For example,
*}
@@ -97,8 +97,8 @@
\begin{warn}
The running time of @{text arith} is exponential in the number of occurrences
- of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
- \isaindexbold{max} because they are first eliminated by case distinctions.
+ of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
+ \cdx{max} because they are first eliminated by case distinctions.
\isa{arith} is incomplete even for the restricted class of
linear arithmetic formulae. If divisibility plays a
--- a/doc-src/TutorialI/Misc/pairs.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/pairs.thy Tue Jul 17 13:46:21 2001 +0200
@@ -1,11 +1,11 @@
(*<*)
theory pairs = Main:;
(*>*)
-text{*\label{sec:pairs}\indexbold{pair}
-HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
+text{*\label{sec:pairs}\index{pairs and tuples}
+HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
-$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
-\isaindexbold{snd}:
+$\tau@i$. The functions \cdx{fst} and
+\cdx{snd} extract the components of a pair:
\isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
@@ -15,7 +15,7 @@
Remarks:
\begin{itemize}
\item
-There is also the type \isaindexbold{unit}, which contains exactly one
+There is also the type \tydx{unit}, which contains exactly one
element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
as a degenerate product with 0 components.
\item
--- a/doc-src/TutorialI/Misc/simp.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy Tue Jul 17 13:46:21 2001 +0200
@@ -53,7 +53,7 @@
proofs seen so far could have been performed
with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
only the first subgoal and may thus need to be repeated --- use
-\isaindex{simp_all} to simplify all subgoals.
+\methdx{simp_all} to simplify all subgoals.
Note that @{text simp} fails if nothing changes.
*}
@@ -134,7 +134,7 @@
Assumptions are simplified in a left-to-right fashion. If an
assumption can help in simplifying one to the left of it, this may get
overlooked. In such cases you have to rotate the assumptions explicitly:
-\isacommand{apply}@{text"(rotate_tac"}~$n$@{text")"}\indexbold{*rotate_tac}
+\isacommand{apply}@{text"("}\methdx{rotate_tac}~$n$@{text")"}
causes a cyclic shift by $n$ positions from right to left, if $n$ is
positive, and from left to right, if $n$ is negative.
Beware that such rotations make proofs quite brittle.
@@ -163,8 +163,8 @@
lemma "xor A (\<not>A)";
txt{*\noindent
-Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
-get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}
+Typically, we begin by unfolding some definitions:
+\indexbold{definitions!unfolding}
*}
apply(simp only:xor_def);
@@ -193,7 +193,7 @@
subsection{*Simplifying {\tt\slshape let}-Expressions*}
text{*\index{simplification!of let-expressions}
-Proving a goal containing \isaindex{let}-expressions almost invariably
+Proving a goal containing \sdx{let}-expressions almost invariably
requires the @{text"let"}-con\-structs to be expanded at some point. Since
@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for a predefined constant
(called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
@@ -260,13 +260,13 @@
txt{*\noindent
@{subgoals[display,indent=0]}
-where \isaindexbold{split_if} is a theorem that expresses splitting of
+where \tdx{split_if} is a theorem that expresses splitting of
@{text"if"}s. Because
case-splitting on @{text"if"}s is almost always the right proof strategy, the
simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}
on the initial goal above.
-This splitting idea generalizes from @{text"if"} to \isaindex{case}.
+This splitting idea generalizes from @{text"if"} to \sdx{case}.
Let us simplify a case analysis over lists:
*}(*<*)by simp(*>*)
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
@@ -338,7 +338,7 @@
The simplifier merely simplifies the condition of an \isa{if} but not the
\isa{then} or \isa{else} parts. The latter are simplified only after the
condition reduces to \isa{True} or \isa{False}, or after splitting. The
- same is true for \isaindex{case}-expressions: only the selector is
+ same is true for \sdx{case}-expressions: only the selector is
simplified at first, until either the expression reduces to one of the
cases or it is split.
\end{warn}\index{*split (method, attr.)|)}
@@ -349,7 +349,7 @@
subsection{*Arithmetic*}
-text{*\index{arithmetic}
+text{*\index{linear arithmetic}
The simplifier routinely solves a small class of linear arithmetic formulae
(over type \isa{nat} and other numeric types): it only takes into account
assumptions and conclusions that are relations
@@ -374,7 +374,8 @@
subsection{*Tracing*}
text{*\indexbold{tracing the simplifier}
Using the simplifier effectively may take a bit of experimentation. Set the
-\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
+\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags}
+to get a better idea of what is going
on:
*}
--- a/doc-src/TutorialI/Misc/types.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/types.thy Tue Jul 17 13:46:21 2001 +0200
@@ -3,7 +3,7 @@
gate = "bool \<Rightarrow> bool \<Rightarrow> bool"
('a,'b)alist = "('a \<times> 'b)list";
-text{*\noindent\indexbold{*types}%
+text{*\noindent
Internally all synonyms are fully expanded. As a consequence Isabelle's
output never contains synonyms. Their main purpose is to improve the
readability of theories. Synonyms can be used just like any other
@@ -15,7 +15,7 @@
subsection{*Constant Definitions*}
-text{*\label{sec:ConstDefinitions}\indexbold{definition}%
+text{*\label{sec:ConstDefinitions}\indexbold{definitions}%
The above constants @{term"nand"} and @{term"xor"} are non-recursive and can
therefore be defined directly by
*}
@@ -24,11 +24,12 @@
xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
text{*\noindent%
-where \isacommand{defs}\indexbold{*defs} is a keyword and
+where \commdx{defs} is a keyword and
@{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
-Declarations and definitions can also be merged
+Declarations and definitions can also be merged in a \commdx{constdefs}
+command:
*}
constdefs nor :: gate
@@ -36,7 +37,7 @@
xor2 :: gate
"xor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";
-text{*\noindent\indexbold{*constdefs}%
-in which case the default name of each definition is $f$@{text"_def"}, where
+text{*\noindent
+The default name of each definition is $f$@{text"_def"}, where
$f$ is the name of the defined constant.*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/Protocol/protocol.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Protocol/protocol.tex Tue Jul 17 13:46:21 2001 +0200
@@ -1,7 +1,9 @@
% $Id$
-\chapter{Case Study: Verifying a Cryptographic Protocol}
+\chapter{Case Study: Verifying a Security Protocol}
\label{chap:crypto}
+\index{protocols!security|(}
+
%crypto primitives
\def\lbb{\mathopen{\{\kern-.30em|}}
\def\rbb{\mathclose{|\kern-.32em\}}}
@@ -46,6 +48,7 @@
\section{The Needham-Schroeder Public-Key Protocol}\label{sec:ns-protocol}
+\index{Needham-Schroeder protocol|(}%
This protocol uses public-key cryptography. Each person has a private key, known only to
himself, and a public key, known to everybody. If Alice wants to send Bob a secret message, she
encrypts it using Bob's public key (which everybody knows), and sends it to Bob. Only Bob has the
@@ -73,7 +76,8 @@
further property: that
$Na$ and~$Nb$ were secrets shared by Alice and Bob. (Many
protocols generate such shared secrets, which can be used
-to lessen the reliance on slow public-key operations.) Lowe found this
+to lessen the reliance on slow public-key operations.)
+Lowe\index{Lowe, Gavin|(} found this
claim to be false: if Alice runs the protocol with someone untrustworthy
(Charlie say), then he can start a new run with another agent (Bob say).
Charlie uses Alice as an oracle, masquerading as
@@ -115,13 +119,15 @@
will Bob. Below, we shall look at parts of this protocol's correctness
proof.
-In ground-breaking work, Lowe~\cite{lowe-fdr} showed how such attacks
+In ground-breaking work, Lowe~\cite{lowe-fdr}\index{Lowe, Gavin|)}
+showed how such attacks
could be found automatically using a model checker. An alternative,
which we shall examine below, is to prove protocols correct. Proofs
can be done under more realistic assumptions because our model does
not have to be finite. The strategy is to formalize the operational
semantics of the system and to prove security properties using rule
-induction.
+induction.%
+\index{Needham-Schroeder protocol|)}
\section{Agents and Messages}
@@ -567,7 +573,7 @@
\rulename{analz_Crypt_if}
\end{isabelle}
The simplifier has also used \isa{Spy_see_priK}, proved in
-\S\ref{sec:regularity}) above, to yield \isa{Ba\ \isasymin \ bad}.
+{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ \isasymin \ bad}.
Recall that this subgoal concerns the case
where the last message to be sent was
@@ -634,6 +640,6 @@
correctly~\cite{paulson-yahalom}. Proofs of real-world protocols follow
the strategy illustrated above, but the subgoals can
be much bigger and there are more of them.
-
+\index{protocols!security|)}
\endinput
--- a/doc-src/TutorialI/Recdef/Induction.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy Tue Jul 17 13:46:21 2001 +0200
@@ -48,7 +48,7 @@
In general, the format of invoking recursion induction is
\begin{quote}
\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
-\end{quote}\index{*induct_tac}%
+\end{quote}\index{*induct_tac (method)}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
name of a function that takes an $n$-tuple. Usually the subgoal will
contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
--- a/doc-src/TutorialI/Recdef/Nested2.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy Tue Jul 17 13:46:21 2001 +0200
@@ -77,7 +77,7 @@
text{*\noindent
or declare them globally
-by giving them the \isaindexbold{recdef_cong} attribute as in
+by giving them the \attrdx{recdef_cong} attribute as in
*}
declare map_cong[recdef_cong]
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Jul 17 13:46:21 2001 +0200
@@ -50,7 +50,7 @@
In general, the format of invoking recursion induction is
\begin{quote}
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
-\end{quote}\index{*induct_tac}%
+\end{quote}\index{*induct_tac (method)}%
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
name of a function that takes an $n$-tuple. Usually the subgoal will
contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Jul 17 13:46:21 2001 +0200
@@ -74,7 +74,7 @@
\begin{isamarkuptext}%
\noindent
or declare them globally
-by giving them the \isaindexbold{recdef_cong} attribute as in%
+by giving them the \attrdx{recdef_cong} attribute as in%
\end{isamarkuptext}%
\isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Rules/rules.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Tue Jul 17 13:46:21 2001 +0200
@@ -77,7 +77,7 @@
be replaced by arbitrary formulas. If we use the rule backwards, Isabelle
tries to unify the current subgoal with the conclusion of the rule, which
has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below,
-\S\ref{sec:unification}.) If successful,
+{\S}\ref{sec:unification}.) If successful,
it yields new subgoals given by the formulas assigned to
\isa{?P} and \isa{?Q}.
@@ -175,7 +175,7 @@
\end{isabelle}
We assume \isa{P\ \isasymor\ Q} and
must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction
-elimination rule, \isa{disjE}\@. We invoke it using \isaindex{erule}, a
+elimination rule, \isa{disjE}\@. We invoke it using \methdx{erule}, a
method designed to work with elimination rules. It looks for an assumption that
matches the rule's first premise. It deletes the matching assumption,
regards the first premise as proved and returns subgoals corresponding to
@@ -408,9 +408,9 @@
also illustrates the \isa{intro} method: a convenient way of
applying introduction rules.
-Negation introduction deduces $\neg P$ if assuming $P$ leads to a
+Negation introduction deduces $\lnot P$ if assuming $P$ leads to a
contradiction. Negation elimination deduces any formula in the
-presence of $\neg P$ together with~$P$:
+presence of $\lnot P$ together with~$P$:
\begin{isabelle}
(?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
\rulenamedx{notI}\isanewline
@@ -418,7 +418,7 @@
\rulenamedx{notE}
\end{isabelle}
%
-Classical logic allows us to assume $\neg P$
+Classical logic allows us to assume $\lnot P$
when attempting to prove~$P$:
\begin{isabelle}
(\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
@@ -426,7 +426,7 @@
\end{isabelle}
\index{contrapositives|(}%
-The implications $P\imp Q$ and $\neg Q\imp\neg P$ are logically
+The implications $P\imp Q$ and $\lnot Q\imp\lnot P$ are logically
equivalent, and each is called the
\textbf{contrapositive} of the other. Four further rules support
reasoning about contrapositives. They differ in the placement of the
@@ -450,7 +450,7 @@
The most important of these is \isa{contrapos_np}. It is useful
for applying introduction rules to negated assumptions. For instance,
-the assumption $\neg(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we
+the assumption $\lnot(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we
might want to use conjunction introduction on it.
Before we can do so, we must move that assumption so that it
becomes the conclusion. The following proof demonstrates this
@@ -586,7 +586,7 @@
instance of~$Q$. It is appropriate for destruction rules.
\item
Method \isa{frule\ R} is like \isa{drule\ R} except that the matching
-assumption is not deleted. (See \S\ref{sec:frule} below.)
+assumption is not deleted. (See {\S}\ref{sec:frule} below.)
\end{itemize}
Other methods apply a rule while constraining some of its
@@ -847,7 +847,7 @@
An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem
modified using~\isa{of}, described in
-\S\ref{sec:forward} below. An advantage of \isa{rule_tac} is that the
+{\S}\ref{sec:forward} below. An advantage of \isa{rule_tac} is that the
instantiations may refer to
\isasymAnd-bound variables in the current subgoal.%
\index{substitution|)}
@@ -1146,7 +1146,7 @@
specify it ourselves. Suitable methods are \isa{rule_tac}, \isa{drule_tac}
and \isa{erule_tac}.
-We have seen (just above, \S\ref{sec:frule}) a proof of this lemma:
+We have seen (just above, {\S}\ref{sec:frule}) a proof of this lemma:
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\
\isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \
@@ -1265,13 +1265,13 @@
A more challenging example illustrates how Isabelle/HOL defines the least number
operator, which denotes the least \isa{x} satisfying~\isa{P}:%
-\index{least number operator}
+\index{least number operator|see{\protect\isa{LEAST}}}
\begin{isabelle}
(LEAST\ x.\ P\ x)\ = (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))
\end{isabelle}
%
-Let us prove the counterpart of \isa{some_equality} for \isa{LEAST}\@.
+Let us prove the counterpart of \isa{some_equality} for \sdx{LEAST}\@.
The first step merely unfolds the definitions (\isa{LeastM} is a
auxiliary operator):
\begin{isabelle}
@@ -1775,7 +1775,7 @@
\subsection{Modifying a Theorem using {\tt\slshape of} and {\tt\slshape THEN}}
Let us reproduce our examples in Isabelle. Recall that in
-\S\ref{sec:recdef-simplification} we declared the recursive function
+{\S}\ref{sec:recdef-simplification} we declared the recursive function
\isa{gcd}:\index{*gcd (constant)|(}
\begin{isabelle}
\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline
@@ -1906,7 +1906,7 @@
\end{warn}
\begin{exercise}
-In \S\ref{sec:subst} the method \isa{subst\ mult_commute} was applied. How
+In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied. How
can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}?
% answer rule (mult_commute [THEN ssubst])
\end{exercise}
@@ -2394,7 +2394,7 @@
%
We use induction: \isa{gcd.induct} is the
induction rule returned by \isa{recdef}. We simplify using
-rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the
+rules proved in {\S}\ref{sec:recdef-simplification}, since rewriting by the
definition of \isa{gcd} can loop.
\begin{isabelle}
\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\
--- a/doc-src/TutorialI/Sets/sets.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex Tue Jul 17 13:46:21 2001 +0200
@@ -324,7 +324,7 @@
\rulenamedx{UN_E}
\end{isabelle}
%
-The following built-in syntax translation (see \S\ref{sec:def-translations})
+The following built-in syntax translation (see {\S}\ref{sec:def-translations})
lets us express the union over a \emph{type}:
\begin{isabelle}
\ \ \ \ \
@@ -368,7 +368,7 @@
Isabelle uses logical equivalences such as those above in automatic proof.
Unions, intersections and so forth are not simply replaced by their
definitions. Instead, membership tests are simplified. For example, $x\in
-A\cup B$ is replaced by $x\in A\vee x\in B$.
+A\cup B$ is replaced by $x\in A\lor x\in B$.
The internal form of a comprehension involves the constant
\cdx{Collect},
@@ -742,7 +742,7 @@
\subsection{The Reflexive and Transitive Closure}
-\index{closure!reflexive and transitive|(}%
+\index{reflexive and transitive closure|(}%
The \textbf{reflexive and transitive closure} of the
relation~\isa{r} is written with a
postfix syntax. In ASCII we write \isa{r\isacharcircum*} and in
@@ -871,7 +871,7 @@
\isa{auto}, \isa{fast} and \isa{best}. Section~\ref{sec:products} will discuss proof
techniques for ordered pairs in more detail.
\end{warn}
-\index{relations|)}\index{closure!reflexive and transitive|)}
+\index{relations|)}\index{reflexive and transitive closure|)}
\section{Well-Founded Relations and Induction}
@@ -902,7 +902,7 @@
complex recursive function definition or induction. The induction rule
returned by
\isacommand{recdef} is good enough for most purposes. We use an explicit
-well-founded induction only in \S\ref{sec:CTL-revisited}.
+well-founded induction only in {\S}\ref{sec:CTL-revisited}.
\end{warn}
Isabelle/HOL declares \cdx{less_than} as a relation object,
@@ -960,11 +960,11 @@
\end{isabelle}
These constructions can be used in a
-\textbf{recdef} declaration (\S\ref{sec:recdef-simplification}) to define
+\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define
the well-founded relation used to prove termination.
The \bfindex{multiset ordering}, useful for hard termination proofs, is
-available in the Library. Baader and Nipkow \cite[\S2.5]{Baader-Nipkow}
+available in the Library. Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow}
discuss it.
\medskip
@@ -1014,7 +1014,7 @@
\begin{warn}
Casual readers should skip the rest of this section. We use fixed point
-operators only in \S\ref{sec:VMC}.
+operators only in {\S}\ref{sec:VMC}.
\end{warn}
The theory applies only to monotonic functions.\index{monotone functions|bold}
@@ -1065,7 +1065,8 @@
gfp\ f%
\rulename{coinduct}
\end{isabelle}
-A \bfindex{bisimulation} is perhaps the best-known concept defined as a
+A \textbf{bisimulation}\index{bisimulations}
+is perhaps the best-known concept defined as a
greatest fixed point. Exhibiting a bisimulation to prove the equality of
two agents in a process algebra is an example of coinduction.
The coinduction rule can be strengthened in various ways; see
--- a/doc-src/TutorialI/ToyList/ToyList.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Tue Jul 17 13:46:21 2001 +0200
@@ -13,8 +13,9 @@
| Cons 'a "'a list" (infixr "#" 65);
text{*\noindent
-The datatype\index{*datatype} \isaindexbold{list} introduces two
-constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
+\index{datatype@\isacommand {datatype} (command)}
+The datatype \tydx{list} introduces two
+constructors \cdx{Nil} and \cdx{Cons}, the
empty~list and the operator that adds an element to the front of a list. For
example, the term \isa{Cons True (Cons False Nil)} is a value of
type @{typ"bool list"}, namely the list with the elements @{term"True"} and
@@ -25,7 +26,8 @@
@{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
alternative syntax is the standard syntax. Thus the list \isa{Cons True
(Cons False Nil)} becomes @{term"True # False # []"}. The annotation
-\isacommand{infixr}\indexbold{*infixr} means that @{text"#"} associates to
+\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
+means that @{text"#"} associates to
the right, i.e.\ the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
and not as @{text"(x # y) # z"}.
The @{text 65} is the priority of the infix @{text"#"}.
@@ -37,7 +39,7 @@
We recommend that novices avoid using
syntax annotations in their own theories.
\end{warn}
-Next, two functions @{text"app"} and \isaindexbold{rev} are declared:
+Next, two functions @{text"app"} and \cdx{rev} are declared:
*}
consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
@@ -67,11 +69,11 @@
\noindent
The equations for @{text"app"} and @{term"rev"} hardly need comments:
@{text"app"} appends two lists and @{term"rev"} reverses a list. The
-keyword \isacommand{primrec}\index{*primrec} indicates that the recursion is
+keyword \commdx{primrec} indicates that the recursion is
of a particularly primitive kind where each recursive call peels off a datatype
constructor from one of the arguments. Thus the
recursion always terminates, i.e.\ the function is \textbf{total}.
-\index{total function}
+\index{functions!total}
The termination requirement is absolutely essential in HOL, a logic of total
functions. If we were to drop it, inconsistencies would quickly arise: the
@@ -125,7 +127,8 @@
theorem rev_rev [simp]: "rev(rev xs) = xs";
-txt{*\index{*theorem|bold}\index{*simp (attribute)|bold}
+txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
+\index{*simp (attribute)|bold}
\noindent
does several things. It
\begin{itemize}
@@ -170,14 +173,15 @@
Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively
defined functions are best established by induction. In this case there is
-not much choice except to induct on @{term"xs"}:
+nothing obvious except induction on @{term"xs"}:
*}
apply(induct_tac xs);
-txt{*\noindent\index{*induct_tac}%
+txt{*\noindent\index{*induct_tac (method)}%
This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
-@{term"tac"} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
+@{term"tac"} stands for \textbf{tactic},\index{tactics}
+a synonym for ``theorem proving function''.
By default, induction acts on the first subgoal. The new proof state contains
two subgoals, namely the base case (@{term[source]Nil}) and the induction step
(@{term[source]Cons}):
@@ -217,21 +221,20 @@
oops
(*>*)
-subsubsection{*First Lemma: @{text"rev(xs @ ys) = (rev ys) @ (rev xs)"}*}
+subsubsection{*First Lemma*}
text{*
-After abandoning the above proof attempt\indexbold{abandon
-proof}\indexbold{proof!abandon} (at the shell level type
-\isacommand{oops}\indexbold{*oops}) we start a new proof:
+\indexbold{abandoning a proof}\indexbold{proofs!abandoning}
+After abandoning the above proof attempt (at the shell level type
+\commdx{oops}) we start a new proof:
*}
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
-txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
-\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
+txt{*\noindent The keywords \commdx{theorem} and
+\commdx{lemma} are interchangeable and merely indicate
the importance we attach to a proposition. Therefore we use the words
-\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
-interchangeably, too.
+\emph{theorem} and \emph{lemma} pretty much interchangeably, too.
There are two variables that we could induct on: @{term"xs"} and
@{term"ys"}. Because @{text"@"} is defined by recursion on
@@ -256,7 +259,7 @@
oops
(*>*)
-subsubsection{*Second Lemma: @{text"xs @ [] = xs"}*}
+subsubsection{*Second Lemma*}
text{*
This time the canonical proof procedure
@@ -275,8 +278,8 @@
done
-text{*\noindent\indexbold{done}%
-As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
+text{*\noindent
+As a result of that final \commdx{done}, Isabelle associates the lemma just proved
with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
if it is obvious from the context that the proof is finished.
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Jul 17 13:46:21 2001 +0200
@@ -15,8 +15,9 @@
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-The datatype\index{*datatype} \isaindexbold{list} introduces two
-constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
+\index{datatype@\isacommand {datatype} (command)}
+The datatype \tydx{list} introduces two
+constructors \cdx{Nil} and \cdx{Cons}, the
empty~list and the operator that adds an element to the front of a list. For
example, the term \isa{Cons True (Cons False Nil)} is a value of
type \isa{bool\ list}, namely the list with the elements \isa{True} and
@@ -27,7 +28,8 @@
\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
alternative syntax is the standard syntax. Thus the list \isa{Cons True
(Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
-\isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
+\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
+means that \isa{{\isacharhash}} associates to
the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
@@ -39,7 +41,7 @@
We recommend that novices avoid using
syntax annotations in their own theories.
\end{warn}
-Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
+Next, two functions \isa{app} and \cdx{rev} are declared:%
\end{isamarkuptext}%
\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
\ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
@@ -65,11 +67,11 @@
\noindent
The equations for \isa{app} and \isa{rev} hardly need comments:
\isa{app} appends two lists and \isa{rev} reverses a list. The
-keyword \isacommand{primrec}\index{*primrec} indicates that the recursion is
+keyword \commdx{primrec} indicates that the recursion is
of a particularly primitive kind where each recursive call peels off a datatype
constructor from one of the arguments. Thus the
recursion always terminates, i.e.\ the function is \textbf{total}.
-\index{total function}
+\index{functions!total}
The termination requirement is absolutely essential in HOL, a logic of total
functions. If we were to drop it, inconsistencies would quickly arise: the
@@ -121,7 +123,8 @@
\end{isamarkuptext}%
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
\begin{isamarkuptxt}%
-\index{*theorem|bold}\index{*simp (attribute)|bold}
+\index{theorem@\isacommand {theorem} (command)|bold}%
+\index{*simp (attribute)|bold}
\noindent
does several things. It
\begin{itemize}
@@ -166,13 +169,14 @@
Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively
defined functions are best established by induction. In this case there is
-not much choice except to induct on \isa{xs}:%
+nothing obvious except induction on \isa{xs}:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
\begin{isamarkuptxt}%
-\noindent\index{*induct_tac}%
+\noindent\index{*induct_tac (method)}%
This tells Isabelle to perform induction on variable \isa{xs}. The suffix
-\isa{tac} stands for \bfindex{tactic}, a synonym for ``theorem proving function''.
+\isa{tac} stands for \textbf{tactic},\index{tactics}
+a synonym for ``theorem proving function''.
By default, induction acts on the first subgoal. The new proof state contains
two subgoals, namely the base case (\isa{Nil}) and the induction step
(\isa{Cons}):
@@ -214,21 +218,20 @@
In order to simplify this subgoal further, a lemma suggests itself.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{First Lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}%
+\isamarkupsubsubsection{First Lemma%
}
%
\begin{isamarkuptext}%
-After abandoning the above proof attempt\indexbold{abandon
-proof}\indexbold{proof!abandon} (at the shell level type
-\isacommand{oops}\indexbold{*oops}) we start a new proof:%
+\indexbold{abandoning a proof}\indexbold{proofs!abandoning}
+After abandoning the above proof attempt (at the shell level type
+\commdx{oops}) we start a new proof:%
\end{isamarkuptext}%
\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
-\noindent The keywords \isacommand{theorem}\index{*theorem} and
-\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
+\noindent The keywords \commdx{theorem} and
+\commdx{lemma} are interchangeable and merely indicate
the importance we attach to a proposition. Therefore we use the words
-\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
-interchangeably, too.
+\emph{theorem} and \emph{lemma} pretty much interchangeably, too.
There are two variables that we could induct on: \isa{xs} and
\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
@@ -249,7 +252,7 @@
embarking on the proof of a lemma usually remains implicit.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Second Lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}%
+\isamarkupsubsubsection{Second Lemma%
}
%
\begin{isamarkuptext}%
@@ -269,8 +272,8 @@
\end{isamarkuptxt}%
\isacommand{done}%
\begin{isamarkuptext}%
-\noindent\indexbold{done}%
-As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
+\noindent
+As a result of that final \commdx{done}, Isabelle associates the lemma just proved
with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
if it is obvious from the context that the proof is finished.
--- a/doc-src/TutorialI/Types/Axioms.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/Axioms.thy Tue Jul 17 13:46:21 2001 +0200
@@ -212,7 +212,7 @@
wford}. Such intersections need not be given a new name but can be created on
the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
represents the intersection of the $C@i$. Such an expression is called a
-\bfindex{sort}, and sorts can appear in most places where we have only shown
+\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
classes so far, for example in type constraints: @{text"'a::{linord,wford}"}.
In fact, @{text"'a::C"} is short for @{text"'a::{C}"}.
However, we do not pursue this rarefied concept further.
--- a/doc-src/TutorialI/Types/Pairs.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/Pairs.thy Tue Jul 17 13:46:21 2001 +0200
@@ -1,9 +1,9 @@
(*<*)theory Pairs = Main:(*>*)
-section{*Pairs*}
+section{*Pairs and Tuples*}
text{*\label{sec:products}
-Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
+Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
repertoire of operations: pairing and the two projections @{term fst} and
@{term snd}. In any non-trivial application of pairs you will find that this
quickly leads to unreadable formulae involving nests of projections. This
--- a/doc-src/TutorialI/Types/Records.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/Records.thy Tue Jul 17 13:46:21 2001 +0200
@@ -19,6 +19,7 @@
following theorems:
*}
+
thm "point.simps"
text {*
Incomprehensible equations: the selectors Xcoord and Ycoord, also "more";
--- a/doc-src/TutorialI/Types/Typedef.thy Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/Typedef.thy Tue Jul 17 13:46:21 2001 +0200
@@ -17,12 +17,14 @@
subsection{*Declaring New Types*}
text{*\label{sec:typedecl}
-The most trivial way of introducing a new type is by a \bfindex{type
+\index{types!declaring|(}%
+\index{typedecl@\isacommand {typedecl} (command)}%
+The most trivial way of introducing a new type is by a \textbf{type
declaration}: *}
typedecl my_new_type
-text{*\noindent\indexbold{*typedecl}%
+text{*\noindent
This does not define @{typ my_new_type} at all but merely introduces its
name. Thus we know nothing about this type, except that it is
non-empty. Such declarations without definitions are
@@ -48,13 +50,16 @@
axioms, in which case you will be able to prove everything but it will mean
nothing. In the example above, the axiomatic approach is
unnecessary: a one-element type called @{typ unit} is already defined in HOL.
+\index{types!declaring|)}
*}
subsection{*Defining New Types*}
text{*\label{sec:typedef}
-Now we come to the most general method of safely introducing a new type, the
-\bfindex{type definition}. All other methods, for example
+\index{types!defining|(}%
+\index{typedecl@\isacommand {typedef} (command)|(}%
+Now we come to the most general means of safely introducing a new type, the
+\textbf{type definition}. All other means, for example
\isacommand{datatype}, are based on it. The principle is extremely simple:
any non-empty subset of an existing type can be turned into a new type. Thus
a type definition is merely a notational device: you introduce a new name for
@@ -70,7 +75,7 @@
typedef three = "{n. n \<le> 2}"
-txt{*\noindent\indexbold{*typedef}%
+txt{*\noindent
In order to enforce that the representing set on the right-hand side is
non-empty, this definition actually starts a proof to that effect:
@{subgoals[display,indent=0]}
@@ -276,7 +281,9 @@
\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
\end{enumerate}
You can now forget about the representation and work solely in terms of the
-abstract functions $F$ and properties $P$.
+abstract functions $F$ and properties $P$.%
+\index{typedecl@\isacommand {typedef} (command)|)}%
+\index{types!defining|)}
*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/document/Axioms.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Tue Jul 17 13:46:21 2001 +0200
@@ -204,7 +204,7 @@
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
the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
represents the intersection of the $C@i$. Such an expression is called a
-\bfindex{sort}, and sorts can appear in most places where we have only shown
+\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
classes so far, for example in type constraints: \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}linord{\isacharcomma}wford{\isacharbraceright}}.
In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}C} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}C{\isacharbraceright}}.
However, we do not pursue this rarefied concept further.
--- a/doc-src/TutorialI/Types/document/Pairs.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Tue Jul 17 13:46:21 2001 +0200
@@ -2,12 +2,12 @@
\begin{isabellebody}%
\def\isabellecontext{Pairs}%
%
-\isamarkupsection{Pairs%
+\isamarkupsection{Pairs and Tuples%
}
%
\begin{isamarkuptext}%
\label{sec:products}
-Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
+Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
repertoire of operations: pairing and the two projections \isa{fst} and
\isa{snd}. In any non-trivial application of pairs you will find that this
quickly leads to unreadable formulae involving nests of projections. This
--- a/doc-src/TutorialI/Types/document/Typedef.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Typedef.tex Tue Jul 17 13:46:21 2001 +0200
@@ -23,12 +23,14 @@
%
\begin{isamarkuptext}%
\label{sec:typedecl}
-The most trivial way of introducing a new type is by a \bfindex{type
+\index{types!declaring|(}%
+\index{typedecl@\isacommand {typedecl} (command)}%
+The most trivial way of introducing a new type is by a \textbf{type
declaration}:%
\end{isamarkuptext}%
\isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type%
\begin{isamarkuptext}%
-\noindent\indexbold{*typedecl}%
+\noindent
This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its
name. Thus we know nothing about this type, except that it is
non-empty. Such declarations without definitions are
@@ -52,7 +54,8 @@
of your development. It is extremely easy to write down contradictory sets of
axioms, in which case you will be able to prove everything but it will mean
nothing. In the example above, the axiomatic approach is
-unnecessary: a one-element type called \isa{unit} is already defined in HOL.%
+unnecessary: a one-element type called \isa{unit} is already defined in HOL.
+\index{types!declaring|)}%
\end{isamarkuptext}%
%
\isamarkupsubsection{Defining New Types%
@@ -60,8 +63,10 @@
%
\begin{isamarkuptext}%
\label{sec:typedef}
-Now we come to the most general method of safely introducing a new type, the
-\bfindex{type definition}. All other methods, for example
+\index{types!defining|(}%
+\index{typedecl@\isacommand {typedef} (command)|(}%
+Now we come to the most general means of safely introducing a new type, the
+\textbf{type definition}. All other means, for example
\isacommand{datatype}, are based on it. The principle is extremely simple:
any non-empty subset of an existing type can be turned into a new type. Thus
a type definition is merely a notational device: you introduce a new name for
@@ -76,7 +81,7 @@
\end{isamarkuptext}%
\isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}%
\begin{isamarkuptxt}%
-\noindent\indexbold{*typedef}%
+\noindent
In order to enforce that the representing set on the right-hand side is
non-empty, this definition actually starts a proof to that effect:
\begin{isabelle}%
@@ -274,6 +279,8 @@
\end{enumerate}
You can now forget about the representation and work solely in terms of the
abstract functions $F$ and properties $P$.%
+\index{typedecl@\isacommand {typedef} (command)|)}%
+\index{types!defining|)}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/numerics.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex Tue Jul 17 13:46:21 2001 +0200
@@ -76,7 +76,7 @@
\end{warn}
\begin{warn}
-\index{recdef@\protect\isacommand{recdef} (command)!and numeric literals}
+\index{recdef@\isacommand {recdef} (command)!and numeric literals}
Numeric literals are not constructors and therefore
must not be used in patterns. For example, this declaration is
rejected:
@@ -434,7 +434,7 @@
Type \isa{real} is only available in the logic HOL-Real, which
is HOL extended with the rather substantial development of the real
numbers. Base your theory upon theory
-\isa{Real}, not the usual \isa{Main}.%
+\thydx{Real}, not the usual \isa{Main}.%
\index{real numbers|)}\index{*real (type)|)}
Launch Isabelle using the command
\begin{verbatim}
--- a/doc-src/TutorialI/Types/types.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/types.tex Tue Jul 17 13:46:21 2001 +0200
@@ -23,16 +23,16 @@
\input{Types/numerics}
-\index{pair|(}
+\index{pairs and tuples|(}
\input{Types/document/Pairs}
-\index{pair|)}
+\index{pairs and tuples|)}
\input{Types/records}
\section{Axiomatic Type Classes}
\label{sec:axclass}
-\index{axiomatic type class|(}
+\index{axiomatic type classes|(}
\index{*axclass|(}
@@ -62,7 +62,7 @@
\input{Types/document/Axioms}
-\index{axiomatic type class|)}
+\index{axiomatic type classes|)}
\index{*axclass|)}
--- a/doc-src/TutorialI/basics.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/basics.tex Tue Jul 17 13:46:21 2001 +0200
@@ -42,8 +42,9 @@
\section{Theories}
\label{sec:Basic:Theories}
+\index{theories|(}%
Working with Isabelle means creating theories. Roughly speaking, a
-\bfindex{theory} is a named collection of types, functions, and theorems,
+\textbf{theory} is a named collection of types, functions, and theorems,
much like a module in a programming language or a specification in a
specification language. In fact, theories in HOL can be either. The general
format of a theory \texttt{T} is
@@ -61,7 +62,7 @@
automatically visible. To avoid name clashes, identifiers can be
\textbf{qualified} by theory names as in \texttt{T.f} and
\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
-reside in a \bfindex{theory file} named \texttt{T.thy}.
+reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.
This tutorial is concerned with introducing you to the different linguistic
constructs that can fill \textit{\texttt{declarations, definitions, and
@@ -78,25 +79,25 @@
proofs are in separate ML files.
\begin{warn}
- HOL contains a theory \isaindexbold{Main}, the union of all the basic
+ HOL contains a theory \thydx{Main}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.
Unless you know what you are doing, always include \isa{Main}
as a direct or indirect parent of all your theories.
-\end{warn}
+\end{warn}%
+\index{theories|)}
\section{Types, Terms and Formulae}
\label{sec:TypesTermsForms}
-\indexbold{type}
Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
logic whose type system resembles that of functional programming languages
-like ML or Haskell. Thus there are
+like ML or Haskell. Thus there are\index{types}
\begin{description}
-\item[base types,] in particular \isaindex{bool}, the type of truth values,
-and \isaindex{nat}, the type of natural numbers.
-\item[type constructors,] in particular \isaindex{list}, the type of
-lists, and \isaindex{set}, the type of sets. Type constructors are written
+\item[base types,] in particular \tydx{bool}, the type of truth values,
+and \tydx{nat}, the type of natural numbers.
+\item[type constructors,] in particular \tydx{list}, the type of
+lists, and \tydx{set}, the type of sets. Type constructors are written
postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
natural numbers. Parentheses around single arguments can be dropped (as in
\isa{nat list}), multiple arguments are separated by commas (as in
@@ -108,7 +109,7 @@
supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
\isasymFun~$\tau$}.
-\item[type variables,]\indexbold{type variable}\indexbold{variable!type}
+\item[type variables,]\indexbold{type variables}\indexbold{variables!type}
denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
function.
@@ -121,37 +122,37 @@
the user, Isabelle infers the type of all variables automatically (this is
called \bfindex{type inference}) and keeps quiet about it. Occasionally
this may lead to misunderstandings between you and the system. If anything
- strange happens, we recommend to set the \rmindex{flag}
- \isaindexbold{show_types} that tells Isabelle to display type information
- that is usually suppressed: simply type
+ strange happens, we recommend that you set the flag\index{flags}
+ \isa{show_types}\index{*show_types (flag)}.
+ Isabelle will then display type information
+ that is usually suppressed. simply type
\begin{ttbox}
ML "set show_types"
\end{ttbox}
\noindent
This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
-which we introduce as we go along,
-can be set and reset in the same manner.\indexbold{flag!(re)setting}
+which we introduce as we go along, can be set and reset in the same manner.%
+\index{flags!setting and resetting}
\end{warn}
-\textbf{Terms}\indexbold{term} are formed as in functional programming by
+\textbf{Terms}\index{terms} are formed as in functional programming by
applying functions to arguments. If \isa{f} is a function of type
\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
infix functions like \isa{+} and some basic constructs from functional
-programming:
+programming, such as conditional expressions:
\begin{description}
-\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
-means what you think it means and requires that
-$b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
-\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}
+\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if (symbol)}
+Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
+\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let (symbol)}
is equivalent to $u$ where all occurrences of $x$ have been replaced by
$t$. For example,
\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
-\indexbold{*case}
+\indexbold{*case (symbol)}
evaluates to $e@i$ if $e$ is of the form $c@i$.
\end{description}
@@ -162,8 +163,8 @@
\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
\isa{\isasymlambda{}x~y~z.~$t$}.
-\textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.
-There are the basic constants \isaindexbold{True} and \isaindexbold{False} and
+\textbf{Formulae}\indexbold{formulae} are terms of type \tydx{bool}.
+There are the basic constants \cdx{True} and \cdx{False} and
the usual logical connectives (in decreasing order of priority):
\indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
\indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
@@ -191,7 +192,7 @@
\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
Despite type inference, it is sometimes necessary to attach explicit
-\textbf{type constraints}\indexbold{type constraint} to a term. The syntax is
+\bfindex{type constraints} to a term. The syntax is
\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
@@ -208,8 +209,8 @@
additional parentheses. In those cases where Isabelle echoes your
input, you can see which parentheses are dropped --- they were superfluous. If
you are unsure how to interpret Isabelle's output because you don't know
-where the (dropped) parentheses go, set the \rmindex{flag}
-\isaindexbold{show_brackets}:
+where the (dropped) parentheses go, set the flag\index{flags}
+\isa{show_brackets}\index{*show_brackets (flag)}:
\begin{ttbox}
ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
\end{ttbox}
@@ -232,8 +233,8 @@
\item
Constructs with an opening but without a closing delimiter bind very weakly
and should therefore be enclosed in parentheses if they appear in subterms, as
-in \isa{(\isasymlambda{}x.~x) = f}. This includes \isaindex{if},
-\isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
+in \isa{(\isasymlambda{}x.~x) = f}. This includes \sdx{if},
+\sdx{let}, \sdx{case}, \isa{\isasymlambda}, and quantifiers.
\item
Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
because \isa{x.x} is always read as a single qualified identifier that
@@ -253,9 +254,10 @@
Isabelle distinguishes free and bound variables just as is customary. Bound
variables are automatically renamed to avoid clashes with free variables. In
-addition, Isabelle has a third kind of variable, called a \bfindex{schematic
- variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
-with a \isa{?}. Logically, an unknown is a free variable. But it may be
+addition, Isabelle has a third kind of variable, called a \textbf{schematic
+ variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},
+which must a~\isa{?} as its first character.
+Logically, an unknown is a free variable. But it may be
instantiated by another term during the proof process. For example, the
mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
which means that Isabelle can instantiate it arbitrarily. This is in contrast
--- a/doc-src/TutorialI/fp.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/fp.tex Tue Jul 17 13:46:21 2001 +0200
@@ -126,8 +126,9 @@
the files have not been modified).
If you suddenly discover that you need to modify a parent theory of your
- current theory, you must first abandon your current theory\indexbold{abandon
- theory}\indexbold{theory!abandon} (at the shell
+ current theory, you must first abandon your current theory%
+ \indexbold{abandoning a theory}\indexbold{theories!abandoning}
+ (at the shell
level type \commdx{kill}). After the parent theory has
been modified, you go back to your original theory. When its first line
\isa{\isacommand{theory}~T~=~\dots~:} is processed, the
@@ -154,12 +155,12 @@
\subsection{Lists}
-\indexbold{*list}
+\index{*list (type)}%
Lists are one of the essential datatypes in computing. Readers of this
tutorial and users of HOL need to be familiar with their basic operations.
Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
-\isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
+\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
The latter contains many further operations. For example, the functions
\cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
element and the remainder of a list. (However, pattern-matching is usually
@@ -205,8 +206,8 @@
\subsection{Primitive Recursion}
Functions on datatypes are usually defined by recursion. In fact, most of the
-time they are defined by what is called \bfindex{primitive recursion}.
-The keyword \isacommand{primrec}\indexbold{*primrec} is followed by a list of
+time they are defined by what is called \textbf{primitive recursion}.
+The keyword \commdx{primrec} is followed by a list of
equations
\[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
such that $C$ is a constructor of the datatype $t$ and all recursive calls of
@@ -230,12 +231,12 @@
\subsection{Natural Numbers}
\label{sec:nat}
-\index{arithmetic|(}
+\index{linear arithmetic|(}
\input{Misc/document/fakenat.tex}
\input{Misc/document/natsum.tex}
-\index{arithmetic|)}
+\index{linear arithmetic|)}
\subsection{Pairs}
@@ -256,17 +257,18 @@
\subsection{Type Synonyms}
-\indexbold{type synonym}
-Type synonyms are similar to those found in ML\@. Their syntax is fairly self
-explanatory:
+\indexbold{type synonyms|(}%
+Type synonyms are similar to those found in ML\@. They are issued by a
+\commdx{types} command:
\input{Misc/document/types.tex}%
Note that pattern-matching is not allowed, i.e.\ each definition must be of
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
Section~{\S}\ref{sec:Simp-with-Defs} explains how definitions are used
-in proofs.
+in proofs.%
+\indexbold{type synonyms|)}
\input{Misc/document/prime_def.tex}
@@ -359,11 +361,14 @@
\section{Advanced Datatypes}
\label{sec:advanced-datatypes}
-\index{*datatype|(}
-\index{*primrec|(}
+\index{datatype@\isacommand {datatype} (command)|(}
+\index{primrec@\isacommand {primrec} (command)|(}
%|)
-This section presents advanced forms of \isacommand{datatype}s.
+This section presents advanced forms of datatypes: mutual and nested
+recursion. A series of examples will culminate in a treatment of the trie
+data structure.
+
\subsection{Mutual Recursion}
\label{sec:datatype-mut-rec}
@@ -412,9 +417,9 @@
expressing the type of \emph{continuous} functions.
There is even a version of LCF on top of HOL,
called HOLCF~\cite{MuellerNvOS99}.
+\index{datatype@\isacommand {datatype} (command)|)}
+\index{primrec@\isacommand {primrec} (command)|)}
-\index{*primrec|)}
-\index{*datatype|)}
\subsection{Case Study: Tries}
\label{sec:Trie}
@@ -472,7 +477,7 @@
\section{Total Recursive Functions}
\label{sec:recdef}
-\index{*recdef|(}
+\index{recdef@\isacommand {recdef} (command)|(}\index{functions!total|(}
Although many total functions have a natural primitive recursive definition,
this is not always the case. Arbitrary total recursive functions can be
@@ -504,4 +509,4 @@
\index{induction!recursion|)}
\index{recursion induction|)}
-\index{*recdef|)}
+\index{recdef@\isacommand {recdef} (command)|)}\index{functions!total|)}
--- a/doc-src/TutorialI/tutorial.ind Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/tutorial.ind Tue Jul 17 13:46:21 2001 +0200
@@ -86,8 +86,8 @@
\indexspace
- \item abandon proof, \bold{11}
- \item abandon theory, \bold{14}
+ \item abandoning a proof, \bold{11}
+ \item abandoning a theory, \bold{14}
\item \isa {abs} (constant), \hyperpage{135}
\item \texttt {abs}, \bold{189}
\item absolute value, \hyperpage{135}
@@ -101,18 +101,16 @@
\item \isacommand {apply} (command), \hyperpage{13}
\item \isa {arg_cong} (theorem), \bold{80}
\item \isa {arith} (method), \hyperpage{21}, \hyperpage{131}
- \item arithmetic, \hyperpage{20--21}, \hyperpage{31}
\item \textsc {ascii} symbols, \bold{189}
\item associative-commutative function, \hyperpage{158}
\item \isa {assumption} (method), \hyperpage{53}
\item assumptions
\subitem renaming, \hyperpage{66--67}
\subitem reusing, \hyperpage{67}
- \item \isa {auto}, \hyperpage{36}
- \item \isa {auto} (method), \hyperpage{76}
+ \item \isa {auto} (method), \hyperpage{36}, \hyperpage{76}
\item \isa {axclass}, \hyperpage{144--150}
\item axiom of choice, \hyperpage{70}
- \item axiomatic type class, \hyperpage{144--150}
+ \item axiomatic type classes, \hyperpage{144--150}
\indexspace
@@ -126,9 +124,9 @@
\item \isa {bij_def} (theorem), \bold{94}
\item bijections, \hyperpage{94}
\item binomial coefficients, \hyperpage{93}
- \item bisimulation, \bold{100}
+ \item bisimulations, \hyperpage{100}
\item \isa {blast} (method), \hyperpage{72--75}
- \item \isa {bool}, \hyperpage{2}, \bold{3}
+ \item \isa {bool} (type), \hyperpage{2, 3}
\item \isa {bspec} (theorem), \bold{92}
\item \isacommand{by} (command), \hyperpage{57}
@@ -138,17 +136,14 @@
\item \isa {card_Pow} (theorem), \bold{93}
\item \isa {card_Un_Int} (theorem), \bold{93}
\item cardinality, \hyperpage{93}
- \item \isa {case}, \bold{3}, \hyperpage{4}, \bold{16},
+ \item \isa {case} (symbol), \bold{3}, \hyperpage{4}, \hyperpage{16},
\hyperpage{30, 31}
\item case distinction, \bold{17}
\item case splits, \bold{29}
- \item \isa {case_tac}, \bold{17}
- \item \isa {case_tac} (method), \hyperpage{85}
+ \item \isa {case_tac} (method), \hyperpage{17}, \hyperpage{85}
\item \isa {clarify} (method), \hyperpage{74}, \hyperpage{76}
\item \isa {clarsimp} (method), \hyperpage{75, 76}
\item \isa {classical} (theorem), \bold{57}
- \item closure
- \subitem reflexive and transitive, \hyperpage{96--98}
\item coinduction, \bold{100}
\item \isa {Collect} (constant), \hyperpage{93}
\item \isa {comp_def} (theorem), \bold{96}
@@ -161,8 +156,8 @@
\item congruence rules, \bold{157}
\item \isa {conjE} (theorem), \bold{55}
\item \isa {conjI} (theorem), \bold{52}
- \item \isa {Cons}, \bold{7}
- \item \isa {constdefs}, \bold{23}
+ \item \isa {Cons} (constant), \hyperpage{7}
+ \item \isacommand {constdefs} (command), \hyperpage{23}
\item contrapositives, \hyperpage{57}
\item converse
\subitem of a relation, \bold{96}
@@ -171,11 +166,12 @@
\indexspace
- \item \isa {datatype}, \hyperpage{7}, \hyperpage{36--42}
+ \item \isacommand {datatype} (command), \hyperpage{7},
+ \hyperpage{36--42}
\item \isacommand {defer} (command), \hyperpage{14}, \hyperpage{84}
- \item definition, \bold{23}
+ \item definitions, \bold{23}
\subitem unfolding, \bold{28}
- \item \isa {defs}, \bold{23}
+ \item \isacommand {defs} (command), \hyperpage{23}
\item descriptions
\subitem definite, \hyperpage{69}
\subitem indefinite, \hyperpage{70}
@@ -186,7 +182,7 @@
\subitem of sets, \bold{90}
\item \isa {disjCI} (theorem), \bold{58}
\item \isa {disjE} (theorem), \bold{54}
- \item \isa {div}, \bold{20}
+ \item \isa {div} (symbol), \hyperpage{20}
\item divides relation, \hyperpage{68}, \hyperpage{78},
\hyperpage{85--87}, \hyperpage{134}
\item division
@@ -196,7 +192,7 @@
\item domain
\subitem of a relation, \hyperpage{96}
\item \isa {Domain_iff} (theorem), \bold{96}
- \item done, \bold{11}
+ \item \isacommand {done} (command), \hyperpage{11}
\item \isa {drule_tac} (method), \hyperpage{60}, \hyperpage{80}
\item \isa {dvd_add} (theorem), \bold{134}
\item \isa {dvd_anti_sym} (theorem), \bold{134}
@@ -209,10 +205,11 @@
\item \isa {Eps} (constant), \hyperpage{93}
\item equality
\subitem of functions, \bold{93}
+ \subitem of records, \hyperpage{143}
\subitem of sets, \bold{90}
\item \isa {equalityE} (theorem), \bold{90}
\item \isa {equalityI} (theorem), \bold{90}
- \item \isa {erule}, \hyperpage{54}
+ \item \isa {erule} (method), \hyperpage{54}
\item \isa {erule_tac} (method), \hyperpage{60}
\item Euclid's algorithm, \hyperpage{85--87}
\item even numbers
@@ -224,25 +221,28 @@
\item \isa {ext} (theorem), \bold{93}
\item extensionality
\subitem for functions, \bold{93, 94}
+ \subitem for records, \hyperpage{143}
\subitem for sets, \bold{90}
\item \ttEXU, \bold{189}
\indexspace
- \item \isa {False}, \bold{3}
+ \item \isa {False} (constant), \hyperpage{3}
\item \isa {fast} (method), \hyperpage{75, 76}
\item \isa {finite} (symbol), \hyperpage{93}
\item \isa {Finites} (constant), \hyperpage{93}
\item fixed points, \hyperpage{100}
- \item flag, \hyperpage{3, 4}, \hyperpage{31}
- \subitem (re)setting, \bold{3}
+ \item flags, \hyperpage{3, 4}, \hyperpage{31}
+ \subitem setting and resetting, \hyperpage{3}
\item \isa {force} (method), \hyperpage{75, 76}
- \item formula, \bold{3}
+ \item formulae, \bold{3}
\item forward proof, \hyperpage{76--82}
\item \isa {frule} (method), \hyperpage{67}
\item \isa {frule_tac} (method), \hyperpage{60}
- \item \isa {fst}, \bold{21}
+ \item \isa {fst} (constant), \hyperpage{21}
\item functions, \hyperpage{93--95}
+ \subitem total, \hyperpage{9}, \hyperpage{45--50}
+ \subitem underdefined, \hyperpage{165}
\indexspace
@@ -256,7 +256,7 @@
\item \isa {hd} (constant), \hyperpage{15}
\item higher-order pattern, \bold{159}
\item Hilbert's $\varepsilon$-operator, \hyperpage{69--71}
- \item {\textit {hypreal}} (type), \hyperpage{137}
+ \item \isa {hypreal} (type), \hyperpage{137}
\indexspace
@@ -266,7 +266,7 @@
\subitem qualified, \bold{2}
\item identity function, \bold{94}
\item identity relation, \bold{96}
- \item \isa {if}, \bold{3}, \hyperpage{4}
+ \item \isa {if} (symbol), \bold{3}, \hyperpage{4}
\item \isa {iff} (attribute), \hyperpage{73, 74}, \hyperpage{86},
\hyperpage{114}
\item \isa {iffD1} (theorem), \bold{78}
@@ -278,18 +278,19 @@
\item \isa {Image_iff} (theorem), \bold{96}
\item \isa {impI} (theorem), \bold{56}
\item implication, \hyperpage{56--57}
- \item \isa {induct_tac}, \hyperpage{10}, \hyperpage{17},
+ \item \isa {induct_tac} (method), \hyperpage{10}, \hyperpage{17},
\hyperpage{50}, \hyperpage{172}
\item induction, \hyperpage{168--175}
\subitem recursion, \hyperpage{49--50}
\subitem structural, \bold{17}
\subitem well-founded, \hyperpage{99}
\item \isacommand {inductive} (command), \hyperpage{111}
- \item inductive definition, \hyperpage{111--129}
+ \item inductive definition
\subitem simultaneous, \hyperpage{125}
+ \item inductive definitions, \hyperpage{111--129}
\item \isacommand {inductive\_cases} (command), \hyperpage{115},
\hyperpage{123}
- \item \isa {infixr}, \bold{8}
+ \item \isacommand{infixr} (annotation), \hyperpage{8}
\item \isa {inj_on_def} (theorem), \bold{94}
\item injections, \hyperpage{94}
\item inner syntax, \bold{9}
@@ -327,58 +328,62 @@
\indexspace
- \item \isa {LEAST}, \bold{21}
- \item least number operator, \hyperpage{69}
- \item lemma, \hyperpage{11}
- \item \isa {lemma}, \bold{11}
+ \item \isa {LEAST} (symbol), \hyperpage{21}, \hyperpage{69}
+ \item least number operator, \see{\protect\isa{LEAST}}{69}
+ \item \isacommand {lemma} (command), \hyperpage{11}
\item \isacommand {lemmas} (command), \hyperpage{77}, \hyperpage{86}
\item \isa {length} (symbol), \hyperpage{15}
\item \isa {length_induct}, \bold{172}
\item \isa {less_than} (constant), \hyperpage{98}
\item \isa {less_than_iff} (theorem), \bold{98}
- \item \isa {let}, \bold{3}, \hyperpage{4}, \hyperpage{29}
+ \item \isa {let} (symbol), \bold{3}, \hyperpage{4}, \hyperpage{29}
\item \isa {lex_prod_def} (theorem), \bold{99}
\item lexicographic product, \bold{99}, \hyperpage{160}
\item {\texttt{lfp}}
\subitem applications of, \see{CTL}{100}
- \item linear arithmetic, \bold{21}, \hyperpage{131}
- \item \isa {list}, \hyperpage{2}, \bold{7}, \bold{15}
+ \item linear arithmetic, \hyperpage{20--21}, \hyperpage{31},
+ \hyperpage{131}
+ \item \isa {List} (theory), \hyperpage{15}
+ \item \isa {list} (type), \hyperpage{2}, \hyperpage{7},
+ \hyperpage{15}
\item \isa {lists_mono} (theorem), \bold{121}
+ \item Lowe, Gavin, \hyperpage{178--179}
\indexspace
- \item \isa {Main}, \bold{2}
+ \item \isa {Main} (theory), \hyperpage{2}
\item major premise, \bold{59}
- \item \isa {max}, \bold{20, 21}
+ \item \isa {max} (constant), \hyperpage{20, 21}
\item measure function, \bold{45}, \bold{98}
\item \isa {measure_def} (theorem), \bold{99}
\item meta-logic, \bold{64}
\item methods, \bold{14}
- \item \isa {min}, \bold{20, 21}
- \item \isa {mod}, \bold{20}
+ \item \isa {min} (constant), \hyperpage{20, 21}
+ \item \isa {mod} (symbol), \hyperpage{20}
\item \isa {mod_div_equality} (theorem), \bold{133}
\item \isa {mod_mult_distrib} (theorem), \bold{133}
\item \emph{modus ponens}, \hyperpage{51}, \hyperpage{56}
\item \isa {mono_def} (theorem), \bold{100}
\item monotone functions, \bold{100}, \hyperpage{123}
\subitem and inductive definitions, \hyperpage{121--122}
+ \item \isa {more} (constant), \hyperpage{140--142}
\item \isa {mp} (theorem), \bold{56}
\item multiset ordering, \bold{99}
\indexspace
- \item \isa {nat}, \hyperpage{2}
- \item \isa {nat} (type), \hyperpage{133--134}
- \item {\textit {nat}} (type), \hyperpage{20}
+ \item \isa {nat} (type), \hyperpage{2}, \hyperpage{20},
+ \hyperpage{133--134}
\item natural deduction, \hyperpage{51--52}
\item natural numbers, \hyperpage{133--134}
+ \item Needham-Schroeder protocol, \hyperpage{177--179}
\item negation, \hyperpage{57--59}
- \item \isa {Nil}, \bold{7}
+ \item \isa {Nil} (constant), \hyperpage{7}
\item \isa {no_asm}, \bold{27}
\item \isa {no_asm_simp}, \bold{27}
\item \isa {no_asm_use}, \bold{28}
\item non-standard reals, \hyperpage{137}
- \item \isa {None}, \bold{22}
+ \item \isa {None} (constant), \bold{22}
\item \isa {notE} (theorem), \bold{57}
\item \isa {notI} (theorem), \bold{57}
\item numeric literals, \hyperpage{132}
@@ -392,8 +397,8 @@
\item \isa {o_def} (theorem), \bold{94}
\item \isa {OF} (attribute), \hyperpage{78--79}
\item \isa {of} (attribute), \hyperpage{77}, \hyperpage{79}
- \item \isa {oops}, \bold{11}
- \item \isa {option}, \bold{22}
+ \item \isacommand {oops} (command), \hyperpage{11}
+ \item \isa {option} (type), \bold{22}
\item ordered rewriting, \bold{158}
\item outer syntax, \bold{9}
\item overloading, \hyperpage{144--146}
@@ -401,7 +406,7 @@
\indexspace
- \item pair, \bold{21}, \hyperpage{137--140}
+ \item pairs and tuples, \hyperpage{21}, \hyperpage{137--140}
\item parent theory, \bold{2}
\item partial function, \hyperpage{164}
\item pattern, higher-order, \bold{159}
@@ -409,14 +414,16 @@
\item permutative rewrite rule, \bold{158}
\item \isacommand {pr} (command), \hyperpage{14}, \hyperpage{83}
\item \isacommand {prefer} (command), \hyperpage{14}, \hyperpage{84}
- \item primitive recursion, \bold{16}
- \item \isa {primrec}, \hyperpage{8}, \bold{16}, \hyperpage{36--42}
- \item product type, \see{pair}{1}
- \item proof
- \subitem abandon, \bold{11}
+ \item primitive recursion, \see{\isacommand{primrec}}{1}
+ \item \isacommand {primrec} (command), \hyperpage{8}, \hyperpage{16},
+ \hyperpage{36--42}
+ \item product type, \see{pairs and tuples}{1}
\item Proof General, \bold{5}
\item proofs
+ \subitem abandoning, \bold{11}
\subitem examples of failing, \hyperpage{71--72}
+ \item protocols
+ \subitem security, \hyperpage{177--187}
\indexspace
@@ -436,28 +443,33 @@
\subitem of a relation, \hyperpage{96}
\item \isa {range} (symbol), \hyperpage{95}
\item \isa {Range_iff} (theorem), \bold{96}
+ \item \isa {Real} (theory), \hyperpage{137}
\item \isa {real} (type), \hyperpage{136--137}
\item real numbers, \hyperpage{136--137}
- \item \isa {recdef}, \hyperpage{45--50}, \hyperpage{160--168}
- \item \isacommand {recdef} (command), \hyperpage{98}
- \item \protect\isacommand{recdef} (command)
+ \item \isacommand {recdef} (command), \hyperpage{45--50},
+ \hyperpage{98}, \hyperpage{160--168}
\subitem and numeric literals, \hyperpage{132}
- \item \isa {recdef_cong}, \bold{164}
+ \item \isa {recdef_cong} (attribute), \hyperpage{164}
\item \isa {recdef_simp}, \bold{47}
\item \isa {recdef_wf}, \bold{162}
+ \item \isacommand {record} (command), \hyperpage{140}
+ \item \isa {record_split} (method), \hyperpage{143}
+ \item records, \hyperpage{140--144}
+ \subitem extensible, \hyperpage{141--142}
\item recursion
\subitem well-founded, \bold{161}
\item recursion induction, \hyperpage{49--50}
\item \isacommand {redo} (command), \hyperpage{14}
+ \item reflexive and transitive closure, \hyperpage{96--98}
\item relations, \hyperpage{95--98}
\subitem well-founded, \hyperpage{98--99}
\item \isa {rename_tac} (method), \hyperpage{66--67}
- \item \isa {rev}, \bold{8}
+ \item \isa {rev} (constant), \hyperpage{8}
\item rewrite rule, \bold{26}
\subitem permutative, \bold{158}
\item rewriting, \bold{26}
\subitem ordered, \bold{158}
- \item \isa {rotate_tac}, \bold{28}
+ \item \isa {rotate_tac} (method), \hyperpage{28}
\item \isa {rtrancl_refl} (theorem), \bold{96}
\item \isa {rtrancl_trans} (theorem), \bold{96}
\item rule induction, \hyperpage{112--114}
@@ -469,20 +481,19 @@
\item \isa {safe} (method), \hyperpage{75, 76}
\item safe rules, \bold{73}
- \item schematic variable, \bold{4}
- \item \isa {set}, \hyperpage{2}
- \item {\textit {set}} (type), \hyperpage{89}
+ \item \isa {set} (type), \hyperpage{2}, \hyperpage{89}
\item set comprehensions, \hyperpage{91--92}
\item \isa {set_ext} (theorem), \bold{90}
\item sets, \hyperpage{89--93}
\subitem finite, \hyperpage{93}
\subitem notation for finite, \bold{91}
- \item \isa {show_brackets}, \bold{4}
- \item \isa {show_types}, \bold{3}
+ \item settings, \see{flags}{1}
+ \item \isa {show_brackets} (flag), \hyperpage{4}
+ \item \isa {show_types} (flag), \hyperpage{3}
\item \texttt {show_types}, \hyperpage{14}
\item \isa {simp} (attribute), \bold{9}, \hyperpage{26}
\item \isa {simp} (method), \bold{26}
- \item \isa {simp_all}, \hyperpage{26}, \hyperpage{36}
+ \item \isa {simp_all} (method), \hyperpage{26}, \hyperpage{36}
\item simplification, \hyperpage{25--32}, \hyperpage{157--160}
\subitem of let-expressions, \hyperpage{29}
\subitem ordered, \bold{158}
@@ -492,20 +503,20 @@
\item \isa {simplified} (attribute), \hyperpage{77}, \hyperpage{79}
\item simplifier, \bold{25}
\item \isa {size} (constant), \hyperpage{15}
- \item \isa {snd}, \bold{21}
+ \item \isa {snd} (constant), \hyperpage{21}
\item \isa {SOME} (symbol), \hyperpage{69}
\item \texttt {SOME}, \bold{189}
- \item \isa {Some}, \bold{22}
+ \item \isa {Some} (constant), \bold{22}
\item \isa {some_equality} (theorem), \bold{69}
\item \isa {someI} (theorem), \bold{70}
\item \isa {someI2} (theorem), \bold{70}
\item \isa {someI_ex} (theorem), \bold{71}
- \item sort, \bold{150}
+ \item sorts, \hyperpage{150}
\item \isa {spec} (theorem), \bold{64}
\item \isa {split} (constant), \bold{137}
\item \isa {split} (method, attr.), \hyperpage{29--31}
\item split rule, \bold{30}
- \item \isa {split_if}, \bold{30}
+ \item \isa {split_if} (theorem), \hyperpage{30}
\item \isa {ssubst} (theorem), \bold{61}
\item structural induction, \bold{17}
\item \isa {subgoal_tac} (method), \hyperpage{81, 82}
@@ -518,43 +529,40 @@
\item \isa {surj_def} (theorem), \bold{94}
\item surjections, \hyperpage{94}
\item \isa {sym} (theorem), \bold{77}
- \item syntax translation, \bold{23}
+ \item syntax translations, \hyperpage{23--24}
\indexspace
- \item tactic, \bold{10}
\item tacticals, \hyperpage{82--83}
- \item term, \bold{3}
+ \item tactics, \hyperpage{10}
\item \isacommand {term} (command), \hyperpage{14}
\item term rewriting, \bold{26}
- \item termination, \see{total function}{1}
+ \item termination, \see{functions, total}{1}
+ \item terms, \hyperpage{3}
\item \isa {THEN} (attribute), \bold{77}, \hyperpage{79},
\hyperpage{86}
- \item theorem, \hyperpage{11}
- \item \isa {theorem}, \bold{9}, \hyperpage{11}
- \item theory, \bold{2}
- \subitem abandon, \bold{14}
- \item theory file, \bold{2}
+ \item \isacommand {theorem} (command), \bold{9}, \hyperpage{11}
+ \item theories, \hyperpage{2}
+ \subitem abandoning, \bold{14}
+ \item theory files, \hyperpage{2}
\item \isacommand {thm} (command), \hyperpage{14}
\item \isa {tl} (constant), \hyperpage{15}
- \item total function, \hyperpage{9}
- \item \isa {trace_simp}, \bold{31}
+ \item \isa {trace_simp} (flag), \hyperpage{31}
\item tracing the simplifier, \bold{31}
\item \isa {trancl_trans} (theorem), \bold{97}
- \item \isa {translations}, \bold{24}
- \item \isa {True}, \bold{3}
- \item tuple, \see{pair}{1}
+ \item \isa {True} (constant), \hyperpage{3}
+ \item tuples, \see{pairs and tuples}{1}
\item \isacommand {typ} (command), \hyperpage{14}
- \item type, \bold{2}
- \item type constraint, \bold{4}
- \item type declaration, \bold{150}
- \item type definition, \bold{151}
+ \item type constraints, \bold{4}
\item type inference, \bold{3}
- \item type synonym, \bold{22}
- \item type variable, \bold{3}
- \item \isa {typedecl}, \bold{151}
- \item \isa {typedef}, \bold{151}
- \item \isa {types}, \bold{23}
+ \item type synonyms, \hyperpage{22--23}
+ \item type variables, \bold{3}
+ \item \isacommand {typedecl} (command), \hyperpage{150}
+ \item \isacommand {typedef} (command), \hyperpage{151--155}
+ \item types, \hyperpage{2}
+ \subitem declaring, \hyperpage{150--151}
+ \subitem defining, \hyperpage{151--155}
+ \item \isacommand {types} (command), \hyperpage{22}
\indexspace
@@ -564,31 +572,30 @@
\item \isa {UN_I} (theorem), \bold{92}
\item \isa {UN_iff} (theorem), \bold{92}
\item \isa {Un_subset_iff} (theorem), \bold{90}
- \item underdefined function, \hyperpage{165}
\item \isacommand {undo} (command), \hyperpage{14}
- \item \isa {unfold}, \bold{28}
\item unification, \hyperpage{60--63}
\item \isa {UNION} (constant), \hyperpage{93}
\item \texttt {Union}, \bold{189}
\item union
\subitem indexed, \hyperpage{92}
\item \isa {Union_iff} (theorem), \bold{92}
- \item \isa {unit}, \bold{22}
- \item unknown, \bold{4}
- \item unknowns, \bold{52}
+ \item \isa {unit} (type), \hyperpage{22}
+ \item unknowns, \hyperpage{4}, \bold{52}
\item unsafe rules, \bold{73}
\item updating a function, \bold{93}
\indexspace
\item variable, \bold{4}
- \subitem schematic, \bold{4}
+ \item variables
+ \subitem schematic, \hyperpage{4}
\subitem type, \bold{3}
\item \isa {vimage_def} (theorem), \bold{95}
\indexspace
\item \isa {wf_induct} (theorem), \bold{99}
- \item \isa {while}, \bold{167}
+ \item \isa {while} (constant), \hyperpage{167}
+ \item \isa {While_Combinator} (theory), \hyperpage{167}
\end{theindex}
--- a/doc-src/TutorialI/tutorial.sty Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/tutorial.sty Tue Jul 17 13:46:21 2001 +0200
@@ -33,7 +33,7 @@
\newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)|bold}}
\newcommand\cldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (class)}}
-\newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} (type)}}
+\newcommand\tydx[1]{\textit{#1}\index{#1@\protect\isa{#1} (type)}}
\newcommand\thydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theory)}}
\newcommand\attrdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (attribute)}}
@@ -52,8 +52,6 @@
\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
-\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}\@}
-\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}\@}
%\newtheorem{theorem}{Theorem}[section]
\newtheorem{Exercise}{Exercise}[section]
--- a/doc-src/TutorialI/tutorial.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/tutorial.tex Tue Jul 17 13:46:21 2001 +0200
@@ -10,9 +10,11 @@
\makeindex
-\index{termination|see{total function}}
-\index{product type|see{pair}}
-\index{tuple|see{pair}}
+\index{primitive recursion|see{\isacommand{primrec}}}
+\index{product type|see{pairs and tuples}}
+\index{termination|see{functions, total}}
+\index{tuples|see{pairs and tuples}}
+\index{settings|see{flags}}
\index{*<*lex*>|see{lexicographic product}}
\underscoreoff