doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy

   @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\
   @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\
-  @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list)
+  @{index_ML CodegenData.add_inline_proc: "string * (theory -> cterm list -> thm list)
     -> theory -> theory"} \\
-  @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list)
+  @{index_ML CodegenData.del_inline_proc: "string -> theory -> theory"} \\
+  @{index_ML CodegenData.add_preproc: "string * (theory -> thm list -> thm list)
     -> theory -> theory"} \\
+  @{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\
   @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list)
     * thm list Susp.T) -> theory -> theory"} \\
   @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
   @{index_ML CodegenData.get_datatype: "theory -> string
     -> ((string * sort) list * (string * typ list) list) option"} \\

      inlining theorem @{text thm} to executable content.
 
   \item @{ML CodegenData.del_inline}~@{text "thm"}~@{text "thy"} remove
      inlining theorem @{text thm} from executable content, if present.
 
-  \item @{ML CodegenData.add_inline_proc}~@{text "f"}~@{text "thy"} adds
-     inline procedure @{text f} to executable content;
+  \item @{ML CodegenData.add_inline_proc}~@{text "(name, f)"}~@{text "thy"} adds
+     inline procedure @{text f} (named @{text name}) to executable content;
      @{text f} is a computation of rewrite rules dependent on
      the current theory context and the list of all arguments
      and right hand sides of the function equations belonging
      to a certain function definition.
 
-  \item @{ML CodegenData.add_preproc}~@{text "f"}~@{text "thy"} adds
-     generic preprocessor @{text f} to executable content;
+  \item @{ML CodegenData.del_inline_proc}~@{text "name"}~@{text "thy"} removes
+     inline procedure named @{text name} from executable content.
+
+  \item @{ML CodegenData.add_preproc}~@{text "(name, f)"}~@{text "thy"} adds
+     generic preprocessor @{text f} (named @{text name}) to executable content;
      @{text f} is a transformation of the function equations belonging
      to a certain function definition, depending on the
      current theory context.
+
+  \item @{ML CodegenData.del_prepproc}~@{text "name"}~@{text "thy"} removes
+     generic preprcoessor named @{text name} from executable content.
 
   \item @{ML CodegenData.add_datatype}~@{text "(name, (spec, cert))"}~@{text "thy"} adds
      a datatype to executable content, with type constructor
      @{text name} and specification @{text spec}; @{text spec} is
      a pair consisting of a list of type variable with sort