--- a/doc-src/TutorialI/Recdef/Induction.thy Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Induction.thy Tue Feb 20 10:37:12 2001 +0100
@@ -47,7 +47,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)"}
+\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
\end{quote}\index{*induct_tac}%
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
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Feb 20 10:37:12 2001 +0100
@@ -49,7 +49,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}}
+\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}%
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
--- a/doc-src/TutorialI/Rules/rules.tex Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Tue Feb 20 10:37:12 2001 +0100
@@ -570,7 +570,7 @@
placeholders for terms. \emph{Unification} refers to the process of
making two terms identical, possibly by replacing their schematic variables by
terms. The simplest case is when the two terms are already the same. Next
-simplest is when the variables in only one of the term
+simplest is when the variables in only one of the terms
are replaced; this is called pattern-matching. The
\isa{rule} method typically matches the rule's conclusion
against the current subgoal. In the most complex case, variables in both
@@ -655,7 +655,7 @@
resulting subgoal is trivial by assumption, so the \isacommand{by} command
proves it implicitly.
-We are using the \isa{erule} method it in a novel way. Hitherto,
+We are using the \isa{erule} method in a novel way. Hitherto,
the conclusion of the rule was just a variable such as~\isa{?R}, but it may
be any term. The conclusion is unified with the subgoal just as
it would be with the \isa{rule} method. At the same time \isa{erule} looks
--- a/doc-src/TutorialI/Sets/sets.tex Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Tue Feb 20 10:37:12 2001 +0100
@@ -374,7 +374,7 @@
\isa{Collect},\index{*Collect (constant)}
which occasionally appears when a goal or theorem
is displayed. For example, \isa{Collect\ P} is the same term as
-\isa{\isacharbraceleft z.\ P\ x\isacharbraceright}. The same thing can
+\isa{\isacharbraceleft x.\ P\ x\isacharbraceright}. The same thing can
happen with quantifiers: \hbox{\isa{All\ P}}\index{*All (constant)}
is
\isa{{\isasymforall}z.\ P\ x} and
--- a/doc-src/TutorialI/appendix.tex Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/appendix.tex Tue Feb 20 10:37:12 2001 +0100
@@ -53,7 +53,7 @@
\ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
\verb$\<exists>!$\\
\indexboldpos{\isasymepsilon}{$HOL0ExSome} &
-\ttindexbold{SOME} &
+\ttindexbold{SOME}, \texttt{\at}\index{$HOL2list@\texttt{\at}} &
\verb$\<epsilon>$\\
\indexboldpos{\isasymcirc}{$HOL1} &
\ttindexbold{o} &
--- a/doc-src/TutorialI/fp.tex Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Tue Feb 20 10:37:12 2001 +0100
@@ -297,7 +297,7 @@
Simplification is one of the central theorem proving tools in Isabelle and
many other systems. The tool itself is called the \bfindex{simplifier}. The
-purpose of this section is introduce the many features of the simplifier.
+purpose of this section is to introduce the many features of the simplifier.
Anybody intending to perform proofs in HOL should read this section. Later on
({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
little bit of how the simplifier works. The serious student should read that
@@ -466,7 +466,7 @@
defined by means of \isacommand{recdef}: you can use full pattern-matching,
recursion need not involve datatypes, and termination is proved by showing
that the arguments of all recursive calls are smaller in a suitable (user
-supplied) sense. In this section we ristrict ourselves to measure functions;
+supplied) sense. In this section we restrict ourselves to measure functions;
more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
\subsection{Defining Recursive Functions}