# HG changeset patch
# User haftmann
# Date 1161594305 -7200
# Node ID cf6defa312095a43eb50d7b1e197d7b8d076fc1f
# Parent  13348ab97f5ab5b741390ae502207c66776899f6
continued

diff -r 13348ab97f5a -r cf6defa31209 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Oct 23 00:52:15 2006 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Oct 23 11:05:05 2006 +0200
@@ -352,7 +352,6 @@
   the file system, with root given by the user.
 *}
 
-ML {* set Toplevel.debug *}
 code_gen dummy (Haskell "examples/")
   (* NOTE: you may use Haskell only once in this document *)
 
@@ -400,15 +399,58 @@
 *}
 
 
-
 section {* Recipes and advanced topics \label{sec:advanced} *}
 
-(* no reference, IsarRef, but see paper *)
+text {*
+  In this tutorial, we do not attempt to give an exhaustive
+  description of the code generator framework; instead,
+  we cast a light on advanced topics by introducing
+  them together with practically motivated examples.  Concerning
+  further reading, see
+
+  \begin{itemize}
+
+  \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
+    for exhaustive syntax diagrams.
+  \item or \fixme{ref} which deals with foundational issues
+    of the code generator framework.
+
+  \end{itemize}
+*}
 
 subsection {* Library theories *}
 
+text {*
+  The HOL \emph{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
+  library; beside being useful in applications, they may serve
+  as a tutorial for cutomizing the code generator setup.
+
+  \begin{description}
+
+    \item[ExecutableSet] allows to generate code
+       for finite sets using lists.
+    \item[ExecutableRat] implements rational
+       numbers as triples @{text "(sign, enumerator, denominator)"}.
+    \item[EfficientNat] implements natural numbers by integers,
+       which in geneal will result in higher efficency; pattern
+       matching with @{const "0\<Colon>nat"} / @{const "Suc"}
+       is eliminated.
+    \item[MLString] provides an additional datatype @{text "mlstring"};
+       in the HOL default setup, strings in HOL are mapped to list
+       of chars in SML; values of type @{text "mlstring"} are
+       mapped to strings in SML.
+
+  \end{description}
+*}
+
 subsection {* Preprocessing *}
 
+text {*
+  
+*}
+
 (* preprocessing, print_codethms () *)
 
 subsection {* Customizing serialization  *}