Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples: (add-dive-into-macro cat expand-address-cat)This feature is used so that the proof-checker's
DV
command and
numeric diving commands (e.g., 3
) will dive properly into subterms.
Please see dive-into-macros-table.