diff -r c6f5cc939c29 -r d33713284207 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Fri Oct 12 08:20:43 2007 +0200
+++ b/doc-src/IsarRef/logics.tex	Fri Oct 12 08:20:45 2007 +0200
@@ -953,7 +953,7 @@
 and \emph{serialization} to a specific \emph{target language}.
 See \cite{isabelle-codegen} for an introduction on how to use it.
 
-\indexisarcmd{code-gen}
+\indexisarcmd{export-code}
 \indexisarcmd{code-thms}
 \indexisarcmd{code-deps}
 \indexisarcmd{code-datatype}
@@ -963,9 +963,9 @@
 \indexisarcmd{code-instance}
 \indexisarcmd{code-monad}
 \indexisarcmd{code-reserved}
+\indexisarcmd{code-include}
 \indexisarcmd{code-modulename}
-\indexisarcmd{code-moduleprolog}
-\indexisarcmd{code-abstype}
+\indexisarcmd{code-exception}
 \indexisarcmd{print-codesetup}
 \indexisaratt{code func}
 \indexisaratt{code inline}
@@ -981,9 +981,9 @@
   \isarcmd{code_instance} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_monad} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_reserved} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_include} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_modulename} & : & \isartrans{theory}{theory} \\
-  \isarcmd{code_moduleprolog} & : & \isartrans{theory}{theory} \\
-  \isarcmd{code_abstype} & : & \isartrans{theory}{theory} \\
+  \isarcmd{code_exception} & : & \isartrans{theory}{theory} \\
   \isarcmd{print_codesetup}^* & : & \isarkeep{theory~|~proof} \\
   code\ func & : & \isaratt \\
   code\ inline & : & \isaratt \\
@@ -1024,15 +1024,15 @@
 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
   ( ( '(' target ( '-' ? + 'and' ) ')' ) + );
 
-'code\_monad' term term term;
+'code\_monad' const const target;
 
 'code\_reserved' target ( string + );
 
+'code\_include' target ( string ( string | '-') );
+
 'code\_modulename' target ( ( string string ) + );
 
-'code\_moduleprolog' target ( ( string ( string | '-') ) + );
-
-'code\_abstype' typ typ 'where' ( const ( '==' | equiv ) const + );
+'code\_exception' ( const + );
 
 syntax : string | ( 'infix' | 'infixl' | 'infixr' ) nat string;
 
@@ -1102,20 +1102,21 @@
   Applies only to \emph{Haskell}.
 
 \item [$\isarcmd{code_monad}$] provides an auxiliary mechanism
-  to generate monad code in \emph{Haskell}.
+  to generate monadic code.
 
 \item [$\isarcmd{code_reserved}$] declares a list of names
   as reserved for a given target, preventing it to be shadowed
   by any generated code.
 
+\item [$\isarcmd{code_include}$] adds arbitrary named content (''include``)
+  to generated code. A as last argument ``-'' will remove an already added ''include``.
+
 \item [$\isarcmd{code_modulename}$] declares aliasings from one module name
   onto another.
 
-\item [$\isarcmd{code_moduleprolog}$] adds an arbitrary content (''prolog``)
-  to a specified module. A ``-'' will remove an already given prolog.
-
-\item [$\isarcmd{code_abstype}$] offers an interface for implementing
-  an abstract type plus operations by executable counterparts.
+\item [$\isarcmd{code_exception}$] declares constants which are not required
+  to have a definition by a defining equations; these are mapped on exceptions
+  instead.
 
 \item [$code\ func$] selects (or with option ''del``, deselects) explicitly
   a defining equation for code generation.  Usually packages introducing