ADD-DIVE-INTO-MACRO
associate
proof-checker
diving function with macro name
Major Section:
EVENTS
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
.