# HG changeset patch
# User wenzelm
# Date 1215552007 -7200
# Node ID 32d18c9b7f212254d691eec3ef8cafbf07082a78
# Parent  c99c72458ec5e2d907069d85400d10b820329085
updated generated file;

diff -r c99c72458ec5 -r 32d18c9b7f21 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Jul 08 23:14:35 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Jul 08 23:20:07 2008 +0200
@@ -78,7 +78,7 @@
   \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
   \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
 
-  \medskip\noindent Type variables are annotated with (finitly many) classes;
+  \medskip\noindent Type variables are annotated with (finitely many) classes;
   these annotations are assertions that a particular polymorphic type
   provides definitions for overloaded functions.
 
@@ -86,7 +86,7 @@
   but form a generic calculus, an instance of order-sorted
   algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
 
-  From a software enigineering point of view, type classes
+  From a software engineering point of view, type classes
   correspond to interfaces in object-oriented languages like Java;
   so, it is naturally desirable that type classes do not only
   provide functions (class parameters) but also state specifications
@@ -102,7 +102,7 @@
   \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
   \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
 
-  \medskip\noindent From a theoretic point of view, type classes are leightweight
+  \medskip\noindent From a theoretic point of view, type classes are lightweight
   modules; Haskell type classes may be emulated by
   SML functors \cite{classes_modules}. 
   Isabelle/Isar offers a discipline of type classes which brings
@@ -324,7 +324,7 @@
 \noindent Associativity from product semigroups is
   established using
   the definition of \isa{{\isasymotimes}} on products and the hypothetical
-  associativety of the type components;  these hypothesis
+  associativity of the type components;  these hypotheses
   are facts due to the \isa{semigroup} constraints imposed
   on the type components by the \isa{instance} proposition.
   Indeed, this pattern often occurs with parametric types
@@ -350,7 +350,7 @@
 \begin{isamarkuptext}%
 \noindent Again, we prove some instances, by
   providing suitable parameter definitions and proofs for the
-  additional specifications.  Obverve that instantiations
+  additional specifications.  Observe that instantiations
   for types with the same arity may be simultaneous:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -775,7 +775,7 @@
   For example, also \isa{list}s form a monoid with
   \isa{op\ {\isacharat}} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
   seems inappropriate to apply to lists
-  the same operations as for genuinly algebraic types.
+  the same operations as for genuinely algebraic types.
   In such a case, we simply can do a particular interpretation
   of monoids for lists:%
 \end{isamarkuptext}%
@@ -945,7 +945,7 @@
 %
 \begin{isamarkuptext}%
 As a commodity, class context syntax allows to refer
-  to local class operations and their global conuterparts
+  to local class operations and their global counterparts
   uniformly;  type inference resolves ambiguities.  For example:%
 \end{isamarkuptext}%
 \isamarkuptrue%