# HG changeset patch
# User haftmann
# Date 1245226035 -7200
# Node ID 6c95ec0394f17cb5f7403dd5c312075f5c905160
# Parent  e1223f58ea9b80b7d75604b22de29ddedae103cf
fixed grammar

diff -r e1223f58ea9b -r 6c95ec0394f1 doc-src/Classes/Thy/Classes.thy
--- a/doc-src/Classes/Thy/Classes.thy	Mon Jun 15 08:16:09 2009 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Wed Jun 17 10:07:15 2009 +0200
@@ -182,8 +182,8 @@
 text {*
   \noindent Note the occurence of the name @{text mult_nat}
   in the primrec declaration;  by default, the local name of
-  a class operation @{text f} to instantiate on type constructor
-  @{text \<kappa>} are mangled as @{text f_\<kappa>}.  In case of uncertainty,
+  a class operation @{text f} to be instantiated on type constructor
+  @{text \<kappa>} is mangled as @{text f_\<kappa>}.  In case of uncertainty,
   these names may be inspected using the @{command "print_context"} command
   or the corresponding ProofGeneral button.
 *}
@@ -191,7 +191,7 @@
 subsection {* Lifting and parametric types *}
 
 text {*
-  Overloaded definitions giving on class instantiation
+  Overloaded definitions given on class instantiation
   may include recursion over the syntactic structure of types.
   As a canonical example, we model product semigroups
   using our simple algebra:
@@ -212,8 +212,7 @@
 end %quote
 
 text {*
-  \noindent Associativity from product semigroups is
-  established using
+  \noindent Associativity of product semigroups is established using
   the definition of @{text "(\<otimes>)"} on products and the hypothetical
   associativity of the type components;  these hypotheses
   are facts due to the @{class semigroup} constraints imposed