doc-src/IsarRef/logics.tex

 \indexisarcmd{print-codesetup}
 \indexisaratt{code func}
 \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} \\
   \isarcmd{code_const} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_type} & : & \isartrans{theory}{theory} \\

   code\ func & : & \isaratt \\
   code\ inline & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
-'code\_gen' ( constexpr + ) ? \\
+'export\_code' ( constexpr + ) ? \\
   ( ( 'in' target ( 'module_name' string ) ? ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
 
 'code\_thms' ( constexpr + ) ?;
 
 'code\_deps' ( constexpr + ) ?;

 'code\ inline' ( 'del' ) ?;
 \end{rail}
 
 \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
   is given, only abstract code is cached.