src/Doc/IsarRef/HOL_Specific.thy

   \end{matharray}
 
   @{rail "
     @@{command (HOL) export_code} ( constexpr + ) \\
        ( ( @'in' target ( @'module_name' @{syntax string} ) ? \\
-        ( @'file' ( @{syntax string} | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
+        ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
     ;
 
     const: @{syntax term}
     ;