--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Apr 25 08:09:10 2000 +0200
@@ -2,10 +2,10 @@
\isacommand{theory}~ToyList~=~PreList:%
\begin{isamarkuptext}%
\noindent
-HOL already has a predefined theory of lists called \texttt{List} ---
-\texttt{ToyList} is merely a small fragment of it chosen as an example. In
+HOL already has a predefined theory of lists called \isa{List} ---
+\isa{ToyList} is merely a small fragment of it chosen as an example. In
contrast to what is recommended in \S\ref{sec:Basic:Theories},
-\texttt{ToyList} is not based on \texttt{Main} but on \texttt{PreList}, a
+\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
theory that contains pretty much everything but lists, thus avoiding
ambiguities caused by defining lists twice.%
\end{isamarkuptext}%
@@ -31,7 +31,7 @@
\begin{warn}
Syntax annotations are a powerful but completely optional feature. You
- could drop them from theory \texttt{ToyList} and go back to the identifiers
+ could drop them from theory \isa{ToyList} and go back to the identifiers
\isa{Nil} and \isa{Cons}. However, lists are such a central datatype
that their syntax is highly customized. We recommend that novices should
not use syntax annotations in their own theories.
@@ -63,7 +63,7 @@
\isa{app} appends two lists and \isa{rev} reverses a list. The keyword
\isacommand{primrec}\index{*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 (see \S\ref{sec:datatype}). Thus the
+constructor from one of the arguments. Thus the
recursion always terminates, i.e.\ the function is \bfindex{total}.
The termination requirement is absolutely essential in HOL, a logic of total
@@ -98,7 +98,7 @@
\begin{isamarkuptext}%
\noindent
When Isabelle prints a syntax error message, it refers to the HOL syntax as
-the \bfindex{inner syntax}.
+the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
\section{An introductory proof}
@@ -116,7 +116,7 @@
\end{isamarkuptext}%
\isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}%
\begin{isamarkuptxt}%
-\noindent\index{*theorem|bold}\index{*simp (attribute)|bold}
+\index{*theorem|bold}\index{*simp (attribute)|bold}
\begin{itemize}
\item
establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs},
@@ -209,8 +209,8 @@
\begin{isamarkuptext}%
\subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
-After abandoning the above proof attempt (at the shell level type
-\isa{oops}) we start a new proof:%
+After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type
+\isacommand{oops}) we start a new proof:%
\end{isamarkuptext}%
\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}%
\begin{isamarkuptxt}%
@@ -220,7 +220,6 @@
\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
interchangeably.
-%FIXME indent!
There are two variables that we could induct on: \isa{xs} and
\isa{ys}. Because \isa{\at} is defined by recursion on
the first argument, \isa{xs} is the correct one:%
@@ -236,9 +235,9 @@
~1.~rev~ys~=~rev~ys~@~[]\isanewline
~2. \dots
\end{isabellepar}%
-We need to cancel this proof attempt and prove another simple lemma first.
-In the future the step of cancelling an incomplete proof before embarking on
-the proof of a lemma often remains implicit.%
+Again, we need to abandon this proof attempt and prove another simple lemma first.
+In the future the step of abandoning an incomplete proof before embarking on
+the proof of a lemma usually remains implicit.%
\end{isamarkuptxt}%
%
\begin{isamarkuptext}%