doc-src/Codegen/Thy/Evaluation.thy

 
 
 subsection {* Evaluation techniques *}
 
 text {*
-  The existing infrastructure provides a rich palett of evaluation
+  The existing infrastructure provides a rich palette of evaluation
   techniques, each comprising different aspects:
 
   \begin{description}
 
     \item[Expressiveness.]  Depending on how good symbolic computation

 
     \item Evaluation of @{term t} terminates with a result @{term
       "t'"}.
 
     \item Evaluation of @{term t} terminates which en exception
-      indicating a pattern match failure or a not-implemented
+      indicating a pattern match failure or a non-implemented
       function.  As sketched in \secref{sec:partiality}, this can be
       interpreted as partiality.
      
     \item Evaluation raises any other kind of exception.
      

   \noindent For conversions, the first case yields the equation @{term
   "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
   Exceptions of the third kind are propagated to the user.
 
   By default return values of plain evaluation are optional, yielding
-  @{text "SOME t'"} in the first case, @{text "NONE"} and in the
-  second propagating the exception in the third case.  A strict
+  @{text "SOME t'"} in the first case, @{text "NONE"} in the
+  second, and propagating the exception in the third case.  A strict
   variant of plain evaluation either yields @{text "t'"} or propagates
   any exception, a liberal variant caputures any exception in a result
   of type @{text "Exn.result"}.
   
   For property conversion (which coincides with conversion except for