--- a/doc-src/Codegen/Thy/Evaluation.thy Wed Nov 03 12:20:33 2010 +0100
+++ b/doc-src/Codegen/Thy/Evaluation.thy Wed Nov 03 14:14:05 2010 +0100
@@ -18,7 +18,7 @@
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}
@@ -135,7 +135,7 @@
"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.
@@ -148,8 +148,8 @@
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"}.
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Wed Nov 03 12:20:33 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Wed Nov 03 14:14:05 2010 +0100
@@ -38,7 +38,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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}
@@ -188,7 +188,7 @@
\item Evaluation of \isa{t} terminates with a result \isa{t{\isacharprime}}.
\item Evaluation of \isa{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.
@@ -200,8 +200,8 @@
Exceptions of the third kind are propagated to the user.
By default return values of plain evaluation are optional, yielding
- \isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} and in the
- second propagating the exception in the third case. A strict
+ \isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} in the
+ second, and propagating the exception in the third case. A strict
variant of plain evaluation either yields \isa{t{\isacharprime}} or propagates
any exception, a liberal variant caputures any exception in a result
of type \isa{Exn{\isachardot}result}.