1.1 --- a/doc-src/HOL/HOL.tex	Sun Mar 03 17:23:45 2002 +0100
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon Mar 04 13:54:41 2002 +0100
     1.3 @@ -3022,9 +3022,9 @@
     1.4  
     1.5  \begin{figure}
     1.6  \begin{rail}
     1.7 -codegen : 'generate_code' ( () | '(' string ')') (code +);
     1.8 -
     1.9 -code : name '=' string;
    1.10 +codegen : 'generate_code' ( () | '(' name ')') (code +);
    1.11 +
    1.12 +code : name '=' term;
    1.13  
    1.14  constscode : 'consts_code' (codespec +);
    1.15  
    1.16 @@ -3064,7 +3064,7 @@
    1.17  calls itself for all subterms.
    1.18  When it arrives at a constant, the default strategy of the code
    1.19  generator is to look up its definition and try to generate code for it.
    1.20 -Some primitive constants of a logic, which have no definitions that
    1.21 +Constants which have no definitions that
    1.22  are immediately executable, may be associated with a piece of ML
    1.23  code manually using the \ttindex{consts_code} command
    1.24  (see Fig.~\ref{fig:HOL:codegen}).
    1.25 @@ -3076,7 +3076,16 @@
    1.26  template using antiquotation brackets \verb|{*|~$\ldots$~\verb|*}|.
    1.27  A similar mechanism is available for
    1.28  types: \ttindex{types_code} associates type constructors with
    1.29 -specific ML code.
    1.30 +specific ML code. For example, the declaration
    1.31 +\begin{ttbox}
    1.32 +types_code
    1.33 +  "*"     ("(_ */ _)")
    1.34 +
    1.35 +consts_code
    1.36 +  "Pair"    ("(_,/ _)")
    1.37 +\end{ttbox}
    1.38 +in theory \texttt{Main} describes how the product type of Isabelle/HOL
    1.39 +should be compiled to ML.
    1.40  
    1.41  Another possibility of configuring the code generator is to register
    1.42  theorems to be used for code generation. Theorems can be registered
    1.43 @@ -3087,6 +3096,13 @@
    1.44  \texttt{ind}). The left-hand sides of equations may only contain
    1.45  constructors and distinct variables, whereas horn clauses must have
    1.46  the same format as introduction rules of inductive definitions.
    1.47 +For example, the declaration
    1.48 +\begin{ttbox}
    1.49 +lemma [code]: "((n::nat) < 0) = False" by simp
    1.50 +declare less_Suc_eq [code]
    1.51 +\end{ttbox}
    1.52 +in theory \texttt{Main} specifies two equations from which to generate
    1.53 +code for \texttt{<} on natural numbers.
    1.54  
    1.55  \subsection{Specific HOL code generators}
    1.56  
    1.57 @@ -3095,13 +3111,31 @@
    1.58  HOL constructs. These include datatypes, recursive functions and
    1.59  inductive relations. The code generator for inductive relations
    1.60  can handle expressions of the form $(t@1,\ldots,t@n) \in r$, where
    1.61 -$r$ is an inductively defined relation. In case at least one of the
    1.62 -$t@i$ is a dummy pattern $_$, the above expression evaluates to a
    1.63 +$r$ is an inductively defined relation. If at least one of the
    1.64 +$t@i$ is a dummy pattern ``$_$'', the above expression evaluates to a
    1.65  sequence of possible answers. If all of the $t@i$ are proper
    1.66 -terms, the expression evaluates to a boolean value. The theory
    1.67 +terms, the expression evaluates to a boolean value.
    1.68 +\begin{small}
    1.69 +\begin{alltt}
    1.70 +  theory Test = Lambda:
    1.71 +
    1.72 +  generate_code
    1.73 +    test1 = "Abs (Var 0) \(\circ\) Var 0 -> Var 0"
    1.74 +    test2 = "Abs (Abs (Var 0 \(\circ\) Var 0) \(\circ\) (Abs (Var 0) \(\circ\) Var 0)) -> _"
    1.75 +\end{alltt}
    1.76 +\end{small}
    1.77 +In the above example, \texttt{test1} evaluates to the boolean
    1.78 +value \texttt{true}, whereas \texttt{test2} is a sequence whose
    1.79 +elements can be inspected using \texttt{Seq.pull} or similar functions.
    1.80 +\begin{ttbox}
    1.81 +ML \{* Seq.pull test2 *\}  -- \{* This is the first answer *\}
    1.82 +ML \{* Seq.pull (snd (the it)) *\}  -- \{* This is the second answer *\}
    1.83 +\end{ttbox}
    1.84 +The theory
    1.85  underlying the HOL code generator is described more detailed in
    1.86 -\cite{Berghofer-Nipkow:2002}.
    1.87 -
    1.88 +\cite{Berghofer-Nipkow:2002}. More examples that illustrate the usage
    1.89 +of the code generator can be found e.g.~in theories
    1.90 +\texttt{MicroJava/J/JListExample} and \texttt{MicroJava/JVM/JVMListExample}.
    1.91  
    1.92  \section{The examples directories}
    1.93