--- a/doc-src/TutorialI/Advanced/WFrec.thy Tue Feb 20 11:27:04 2001 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Tue Feb 20 13:23:58 2001 +0100
@@ -1,7 +1,7 @@
(*<*)theory WFrec = Main:(*>*)
text{*\noindent
-So far, all recursive definitions where shown to terminate via measure
+So far, all recursive definitions were shown to terminate via measure
functions. Sometimes this can be quite inconvenient or even
impossible. Fortunately, \isacommand{recdef} supports much more
general definitions. For example, termination of Ackermann's function
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Tue Feb 20 11:27:04 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Tue Feb 20 13:23:58 2001 +0100
@@ -4,7 +4,7 @@
%
\begin{isamarkuptext}%
\noindent
-So far, all recursive definitions where shown to terminate via measure
+So far, all recursive definitions were shown to terminate via measure
functions. Sometimes this can be quite inconvenient or even
impossible. Fortunately, \isacommand{recdef} supports much more
general definitions. For example, termination of Ackermann's function
--- a/doc-src/TutorialI/Types/Overloading1.thy Tue Feb 20 11:27:04 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading1.thy Tue Feb 20 13:23:58 2001 +0100
@@ -50,7 +50,7 @@
More interesting \isacommand{instance} proofs will arise below
in the context of proper axiomatic type classes.
-Althoug terms like @{prop"False <<= P"} are now legal, we still need to say
+Although terms like @{prop"False <<= P"} are now legal, we still need to say
what the relation symbols actually mean at type @{typ bool}:
*}
--- a/doc-src/TutorialI/Types/Pairs.thy Tue Feb 20 11:27:04 2001 +0100
+++ b/doc-src/TutorialI/Types/Pairs.thy Tue Feb 20 13:23:58 2001 +0100
@@ -6,7 +6,7 @@
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 involvings nests of projections. This
+quickly leads to unreadable formulae involving nests of projections. This
section is concerned with introducing some syntactic sugar to overcome this
problem: pattern matching with tuples.
*}
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Tue Feb 20 11:27:04 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Tue Feb 20 13:23:58 2001 +0100
@@ -48,7 +48,7 @@
More interesting \isacommand{instance} proofs will arise below
in the context of proper axiomatic type classes.
-Althoug terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say
+Although terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say
what the relation symbols actually mean at type \isa{bool}:%
\end{isamarkuptext}%
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
--- a/doc-src/TutorialI/Types/document/Pairs.tex Tue Feb 20 11:27:04 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Tue Feb 20 13:23:58 2001 +0100
@@ -10,7 +10,7 @@
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 involvings nests of projections. This
+quickly leads to unreadable formulae involving nests of projections. This
section is concerned with introducing some syntactic sugar to overcome this
problem: pattern matching with tuples.%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Types/numerics.tex Tue Feb 20 11:27:04 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Tue Feb 20 13:23:58 2001 +0100
@@ -183,7 +183,7 @@
As a concession to convention, these equations are not installed as default
simplification rules but are merely used to remove nonzero-divisor
hypotheses by case analysis. In \isa{div_mult_mult1} above, one of
-the two divisors (namely~\isa{c}) must be still be nonzero.
+the two divisors (namely~\isa{c}) must still be nonzero.
The \textbf{divides} relation has the standard definition, which
is overloaded over all numeric types:
--- a/doc-src/TutorialI/Types/types.tex Tue Feb 20 11:27:04 2001 +0100
+++ b/doc-src/TutorialI/Types/types.tex Tue Feb 20 13:23:58 2001 +0100
@@ -43,7 +43,7 @@
Isabelle offers the related concept of an \textbf{axiomatic type class}.
Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\
an axiomatic specification of a class of types. Thus we can talk about a type
-$t$ being in a class $c$, which is written $\tau :: c$. This is the case of
+$t$ being in a class $c$, which is written $\tau :: c$. This is the case if
$\tau$ satisfies the axioms of $c$. Furthermore, type classes can be
organized in a hierarchy. Thus there is the notion of a class $d$ being a
\textbf{subclass} of a class $c$, written $d < c$. This is the case if all