--- a/doc-src/IsarRef/logics.tex Mon Aug 20 18:07:31 2007 +0200
+++ b/doc-src/IsarRef/logics.tex Mon Aug 20 18:07:49 2007 +0200
@@ -776,7 +776,7 @@
\indexisaratt{code inline}
\begin{matharray}{rcl}
- \isarcmd{code_gen}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{export_code}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\
@@ -795,7 +795,7 @@
\end{matharray}
\begin{rail}
-'code\_gen' ( constexpr + ) ? \\
+'export\_code' ( constexpr + ) ? \\
( ( 'in' target ( 'module_name' string ) ? ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
'code\_thms' ( constexpr + ) ?;
@@ -849,7 +849,7 @@
\begin{descr}
-\item [$\isarcmd{code_gen}$] is the canonical interface for generating and
+\item [$\isarcmd{export_code}$] is the canonical interface for generating and
serializing code: for a given list of constants, code is generated for the specified
target language(s). Abstract code is cached incrementally. If no constant is given,
the currently cached code is serialized. If no serialization instruction