Removes association of proof-builder diving function with macro name
Example: (remove-dive-into-macro logand)
This feature undoes the effect of add-dive-into-macro, which is used so that the interactive proof-builder's DV command and numeric diving commands (e.g., 3) will dive properly into subterms. Please see add-dive-into-macro and especially see dive-into-macros-table.
