REMOVE-DIVE-INTO-MACRO

removes association of proof-checker diving function with macro name 
Major Section:  SWITCHES-PARAMETERS-AND-MODES


Example:
(remove-dive-into-macro logand)
This feature undoes the effect of add-dive-into-macro, which is used so that the proof-checker'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.