A macro for automatically introducing ACL2::redundant-events, which is useful for developing "interface" books and otherwise avoiding copying and pasting code.
