--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Aug 18 09:55:00 2010 +0200
@@ -55,10 +55,11 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-In a HOL theory, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form the
- core of a functional programming language. By default equational
- theorems stemming from those are used for generated code, therefore
- \qt{naive} code generation can proceed without further ado.
+In a HOL theory, the \indexdef{}{command}{datatype}\hypertarget{command.datatype}{\hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}} and \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}/\indexdef{}{command}{primrec}\hypertarget{command.primrec}{\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}}/\indexdef{}{command}{fun}\hypertarget{command.fun}{\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}} declarations
+ form the core of a functional programming language. By default
+ equational theorems stemming from those are used for generated code,
+ therefore \qt{naive} code generation can proceed without further
+ ado.
For example, here a simple \qt{implementation} of amortised queues:%
\end{isamarkuptext}%
@@ -184,12 +185,12 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated
- list of constants for which code shall be generated; anything else
- needed for those is added implicitly. Then follows a target
- language identifier and a freely chosen module name. A file name
- denotes the destination to store the generated code. Note that the
- semantics of the destination depends on the target language: for
+\noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a
+ space-separated list of constants for which code shall be generated;
+ anything else needed for those is added implicitly. Then follows a
+ target language identifier and a freely chosen module name. A file
+ name denotes the destination to store the generated code. Note that
+ the semantics of the destination depends on the target language: for
\isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell} it denotes a \emph{directory} where a file named as the
module name (with extension \isa{{\isachardot}hs}) is written:%
\end{isamarkuptext}%