remove the association of a binary function name with a macro name
Major Section:  EVENTS

(remove-binop binary-append)

General Form: (remove-binop binop)

See add-binop for a discussion of how to associate a macro name with a binary function name for proof output purposes. This form sets binop-table to the result of deleting the association of a macro name with the given binary function name. If the function name has no such association, then this form still generates an event, but the event has no real effect.