# HG changeset patch
# User haftmann
# Date 1285223433 -7200
# Node ID 29cc021398fcfa8776d0ca9058e298979fe2614b
# Parent  dd7b582f6929c95b8f2a553c2d1fc2834665eb63
corrections and tuning

diff -r dd7b582f6929 -r 29cc021398fc doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy	Wed Sep 22 18:40:35 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Thu Sep 23 08:30:33 2010 +0200
@@ -260,7 +260,7 @@
   to introduce inconsistencies -- or, in other words: custom
   serialisations are completely axiomatic.
 
-  A further noteworthy details is that any special character in a
+  A further noteworthy detail is that any special character in a
   custom serialisation may be quoted using ``@{verbatim "'"}''; thus,
   in ``@{verbatim "fn '_ => _"}'' the first ``@{verbatim "_"}'' is a
   proper underscore while the second ``@{verbatim "_"}'' is a
@@ -274,13 +274,13 @@
   For convenience, the default @{text HOL} setup for @{text Haskell}
   maps the @{class equal} class to its counterpart in @{text Haskell},
   giving custom serialisations for the class @{class equal} (by command
-  @{command_def code_class}) and its operation @{const HOL.equal}
+  @{command_def code_class}) and its operation @{const [source] HOL.equal}
 *}
 
 code_class %quotett equal
   (Haskell "Eq")
 
-code_const %quotett "op ="
+code_const %quotett "HOL.equal"
   (Haskell infixl 4 "==")
 
 text {*
diff -r dd7b582f6929 -r 29cc021398fc doc-src/Codegen/Thy/Evaluation.thy
--- a/doc-src/Codegen/Thy/Evaluation.thy	Wed Sep 22 18:40:35 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy	Thu Sep 23 08:30:33 2010 +0200
@@ -71,7 +71,7 @@
   inherits from \emph{SML} but for convenience uses parts of the
   Isabelle runtime environment.  The soundness of computation carried
   out there depends crucially on the correctness of the code
-  generator; this is one of the reasons why you should not use
+  generator setup; this is one of the reasons why you should not use
   adaptation (see \secref{sec:adaptation}) frivolously.
 *}
 
@@ -139,13 +139,13 @@
       function.  As sketched in \secref{sec:partiality}, this can be
       interpreted as partiality.
      
-    \item Evaluation raise any other kind of exception.
+    \item Evaluation raises any other kind of exception.
      
   \end{itemize}
 
   \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 propagted to the user.
+  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
@@ -218,9 +218,9 @@
   after the whole ML is read, the necessary code is generated
   transparently and the corresponding constant names are inserted.
   This technique also allows to use pattern matching on constructors
-  stemming from compiled @{text "datatypes"}.  Note that it is not
-  possible to refer to constants which carry adaptations by means of
-  @{text code}; here you have to refer to the adapted code directly.
+  stemming from compiled datatypes.  Note that the @{text code}
+  antiquotation may not refer to constants which carry adaptations;
+  here you have to refer to the corresponding adapted code directly.
 
   For a less simplistic example, theory @{text Approximation} in
   the @{text Decision_Procs} session is a good reference.
@@ -272,7 +272,7 @@
   file "examples/rat.ML"
 
 text {*
-  \noindent This just generates the references code to the specified
+  \noindent This merely generates the referenced code to the given
   file which can be included into the system runtime later on.
 *}
 
diff -r dd7b582f6929 -r 29cc021398fc doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Wed Sep 22 18:40:35 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Thu Sep 23 08:30:33 2010 +0200
@@ -485,7 +485,7 @@
   to introduce inconsistencies -- or, in other words: custom
   serialisations are completely axiomatic.
 
-  A further noteworthy details is that any special character in a
+  A further noteworthy detail is that any special character in a
   custom serialisation may be quoted using ``\verb|'|''; thus,
   in ``\verb|fn '_ => _|'' the first ``\verb|_|'' is a
   proper underscore while the second ``\verb|_|'' is a
@@ -501,7 +501,7 @@
 For convenience, the default \isa{HOL} setup for \isa{Haskell}
   maps the \isa{equal} class to its counterpart in \isa{Haskell},
   giving custom serialisations for the class \isa{equal} (by command
-  \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}}) and its operation \isa{equal{\isacharunderscore}class{\isachardot}equal}%
+  \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}}) and its operation \isa{HOL{\isachardot}equal}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -515,7 +515,7 @@
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}HOL{\isachardot}equal{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
 \endisatagquotett
 {\isafoldquotett}%
diff -r dd7b582f6929 -r 29cc021398fc doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Wed Sep 22 18:40:35 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Thu Sep 23 08:30:33 2010 +0200
@@ -97,7 +97,7 @@
   inherits from \emph{SML} but for convenience uses parts of the
   Isabelle runtime environment.  The soundness of computation carried
   out there depends crucially on the correctness of the code
-  generator; this is one of the reasons why you should not use
+  generator setup; this is one of the reasons why you should not use
   adaptation (see \secref{sec:adaptation}) frivolously.%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -192,12 +192,12 @@
       function.  As sketched in \secref{sec:partiality}, this can be
       interpreted as partiality.
      
-    \item Evaluation raise any other kind of exception.
+    \item Evaluation raises any other kind of exception.
      
   \end{itemize}
 
   \noindent For conversions, the first case yields the equation \isa{t\ {\isacharequal}\ t{\isacharprime}}, the second defaults to reflexivity \isa{t\ {\isacharequal}\ t}.
-  Exceptions of the third kind are propagted to the user.
+  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
@@ -315,9 +315,9 @@
   after the whole ML is read, the necessary code is generated
   transparently and the corresponding constant names are inserted.
   This technique also allows to use pattern matching on constructors
-  stemming from compiled \isa{datatypes}.  Note that it is not
-  possible to refer to constants which carry adaptations by means of
-  \isa{code}; here you have to refer to the adapted code directly.
+  stemming from compiled datatypes.  Note that the \isa{code}
+  antiquotation may not refer to constants which carry adaptations;
+  here you have to refer to the corresponding adapted code directly.
 
   For a less simplistic example, theory \isa{Approximation} in
   the \isa{Decision{\isacharunderscore}Procs} session is a good reference.%
@@ -399,7 +399,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent This just generates the references code to the specified
+\noindent This merely generates the referenced code to the given
   file which can be included into the system runtime later on.%
 \end{isamarkuptext}%
 \isamarkuptrue%