# 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 \} are mangled as @{text f_\}. In case of uncertainty, + a class operation @{text f} to be instantiated on type constructor + @{text \} is mangled as @{text f_\}. 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 "(\)"} on products and the hypothetical associativity of the type components; these hypotheses are facts due to the @{class semigroup} constraints imposed