# HG changeset patch
# User haftmann
# Date 1282118877 -7200
# Node ID 9cea8a0e925a4571afc99139e7b6acfb340a05bd
# Parent  7b34c51b05a4de634fee2a7b31c39b2e012bad49
updated generated document

diff -r 7b34c51b05a4 -r 9cea8a0e925a doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Wed Aug 18 10:07:56 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Wed Aug 18 10:07:57 2010 +0200
@@ -577,7 +577,7 @@
 \begin{isamarkuptext}%
 \noindent The code generator would produce an additional instance,
   which of course is rejected by the \isa{Haskell} compiler.  To
-  suppress this additional instance, use \isa{code{\isacharunderscore}instance}:%
+  suppress this additional instance, use \indexdef{}{command}{code\_instance}\hypertarget{command.code-instance}{\hyperlink{command.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 7b34c51b05a4 -r 9cea8a0e925a doc-src/Codegen/Thy/document/Further.tex
--- a/doc-src/Codegen/Thy/document/Further.tex	Wed Aug 18 10:07:56 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex	Wed Aug 18 10:07:57 2010 +0200
@@ -415,8 +415,9 @@
   \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
   \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
   \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
-  \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
-\verb|    -> theory -> theory| \\
+  \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: |\isasep\isanewline%
+\verb|    string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
+\verb|      -> theory -> theory| \\
   \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
   \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
   \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
diff -r 7b34c51b05a4 -r 9cea8a0e925a doc-src/Codegen/Thy/document/Inductive_Predicate.tex
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex	Wed Aug 18 10:07:56 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex	Wed Aug 18 10:07:57 2010 +0200
@@ -37,7 +37,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The \isa{predicate{\isacharunderscore}compiler} is an extension of the code generator
+The \isa{predicate\ compiler} is an extension of the code generator
   which turns inductive specifications into equational ones, from
   which in turn executable code can be generated.  The mechanisms of
   this compiler are described in detail in