# HG changeset patch
# User haftmann
# Date 1288790045 -3600
# Node ID 1ef7ee8dd165b19646736b47d03f5610599ea560
# Parent  131cf8790a1c4f195380ea77026cfa2cd6476a45
fixed typos

diff -r 131cf8790a1c -r 1ef7ee8dd165 doc-src/Codegen/Thy/Evaluation.thy
--- 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"}.
diff -r 131cf8790a1c -r 1ef7ee8dd165 doc-src/Codegen/Thy/document/Evaluation.tex
--- 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}.