# HG changeset patch
# User nipkow
# Date 982671838 -3600
# Node ID 166f7d87b37f62910517215b5b5a215a5004b82a
# Parent  e0ab13bec5c8cbf8a8a02b5938f143be77cb1deb
*** empty log message ***

diff -r e0ab13bec5c8 -r 166f7d87b37f doc-src/TutorialI/Advanced/WFrec.thy
--- 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
diff -r e0ab13bec5c8 -r 166f7d87b37f doc-src/TutorialI/Advanced/document/WFrec.tex
--- 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
diff -r e0ab13bec5c8 -r 166f7d87b37f doc-src/TutorialI/Types/Overloading1.thy
--- 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}:
 *}
 
diff -r e0ab13bec5c8 -r 166f7d87b37f doc-src/TutorialI/Types/Pairs.thy
--- 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.
 *}
diff -r e0ab13bec5c8 -r 166f7d87b37f doc-src/TutorialI/Types/document/Overloading1.tex
--- 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
diff -r e0ab13bec5c8 -r 166f7d87b37f doc-src/TutorialI/Types/document/Pairs.tex
--- 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}%
diff -r e0ab13bec5c8 -r 166f7d87b37f doc-src/TutorialI/Types/numerics.tex
--- 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: 
diff -r e0ab13bec5c8 -r 166f7d87b37f doc-src/TutorialI/Types/types.tex
--- 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