--- 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 {*
--- 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.
*}
--- 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}%
--- 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%