Open BenHocking opened 2 years ago
(See issue #83 for context)
Because macros imported from other theories can cause name conflicts, it would be very useful to be able to disable them, possibly using MACRO- to mirror the AUTO_REWRITE- functionality one uses to disable previously invoked AUTO_REWRITE commands.
MACRO-
AUTO_REWRITE-
AUTO_REWRITE
(See issue #83 for context)
Because macros imported from other theories can cause name conflicts, it would be very useful to be able to disable them, possibly using
MACRO-to mirror theAUTO_REWRITE-functionality one uses to disable previously invokedAUTO_REWRITEcommands.