# HG changeset patch # User huffman # Date 1215548712 -7200 # Node ID ddd1e71adbfc77fcc20d19b70353377f25eba3b1 # Parent 5287623e7ff993d3335f6741a45b81890760a568 fix more typos diff -r 5287623e7ff9 -r ddd1e71adbfc doc-src/IsarAdvanced/Classes/Thy/Classes.thy --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Jul 08 22:07:39 2008 +0200 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Jul 08 22:25:12 2008 +0200 @@ -91,7 +91,7 @@ \hspace*{4ex}@{text "sym: eq x y \ eq x y"} \\ \hspace*{4ex}@{text "trans: eq x y \ eq y z \ 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 @@ -239,7 +239,7 @@ \noindent Associativity from product semigroups is established using the definition of @{text \} on products and the hypothetical - associativety of the type components; these hypothesis + associativity of the type components; these hypotheses are facts due to the @{text semigroup} constraints imposed on the type components by the @{text instance} proposition. Indeed, this pattern often occurs with parametric types @@ -263,7 +263,7 @@ text {* \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: *} @@ -477,7 +477,7 @@ For example, also @{text "list"}s form a monoid with @{term "op @"} and @{term "[]"} 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: *} @@ -585,7 +585,7 @@ text {* 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: *}