doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Wed Oct 11 08:57:47 2006 +0200
@@ -0,0 +1,99 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Codegen}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Codegen\isanewline
+\isakeyword{imports}\ Main\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Code generation from Isabelle theories%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Introduction%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\cite{isa-tutorial}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Basics%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Invoking the code generator%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Theorem selection%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Type classes%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Preprocessing%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Incremental code generation%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Customizing serialization%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Recipes and advanced topics%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{ML interfaces%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{codegen\_data.ML%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Implementing code generator applications%
+}
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: