--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu May 10 04:06:56 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu May 10 10:21:44 2007 +0200
@@ -106,7 +106,7 @@
by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
So, for the moment, there are two distinct code generators
in Isabelle.
- Also note that while the framework itself is largely
+ Also note that while the framework itself is
object-logic independent, only \isa{HOL} provides a reasonable
framework setup.
\end{warn}%
@@ -118,7 +118,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-When writing executable specifications, it is convenient to use
+When writing executable specifications using \isa{HOL},
+ it is convenient to use
three existing packages: the datatype package for defining
datatypes, the function package for (recursive) functions,
and the class package for overloaded definitions.
@@ -241,7 +242,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Thanks to a reasonable setup of the HOL theories, in
+Thanks to a reasonable setup of the \isa{HOL} theories, in
most cases code generation proceeds without further ado:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -330,7 +331,7 @@
defining equations (the additional stuff displayed
shall not bother us for the moment).
- The typical HOL tools are already set up in a way that
+ The typical \isa{HOL} tools are already set up in a way that
function definitions introduced by \isa{{\isasymDEFINITION}},
\isa{{\isasymFUN}},
\isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}},
@@ -571,17 +572,18 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The HOL \emph{Main} theory already provides a code generator setup
+The \isa{HOL} \isa{Main} theory already provides a code
+ generator setup
which should be suitable for most applications. Common extensions
- and modifications are available by certain theories of the HOL
+ and modifications are available by certain theories of the \isa{HOL}
library; beside being useful in applications, they may serve
as a tutorial for customizing the code generator setup.
\begin{description}
- \item[\isa{Pretty{\isacharunderscore}Int}] represents HOL integers by big
+ \item[\isa{Pretty{\isacharunderscore}Int}] represents \isa{HOL} integers by big
integer literals in target languages.
- \item[\isa{Pretty{\isacharunderscore}Char}] represents HOL characters by
+ \item[\isa{Pretty{\isacharunderscore}Char}] represents \isa{HOL} characters by
character literals in target languages.
\item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr},
but also offers treatment of character codes; includes
@@ -595,11 +597,18 @@
matching with \isa{{\isadigit{0}}} / \isa{Suc}
is eliminated; includes \isa{Pretty{\isacharunderscore}Int}.
\item[\isa{MLString}] provides an additional datatype \isa{mlstring};
- in the HOL default setup, strings in HOL are mapped to list
- of HOL characters in SML; values of type \isa{mlstring} are
+ in the \isa{HOL} default setup, strings in HOL are mapped to list
+ of \isa{HOL} characters in SML; values of type \isa{mlstring} are
mapped to strings in SML.
- \end{description}%
+ \end{description}
+
+ \begin{warn}
+ When importing any of these theories, they should form the last
+ items in an import list. Since these theories adapt the
+ code generator setup in a non-conservative fashion,
+ strange effects may occur otherwise.
+ \end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%