|
|
|---|
|
|
|
|---|
A macro that detects the changes in the theory when a book is included, and creates a macro to enable users to enable and disable the new theory.
Gives users the ability to undo and redo the changes an event, such as include-book, makes to current theory.
(fetch-new-theory <event> ;; e.g., (include-book "arithmetic-5" :dir :system) <macro-name> ;; e.g., use-aritmetic-5 ;;optional key :disabled <disabled> ;; When non-nil, the event does not change the current theory. Default: nil. )
After including the arithmetic library as given below, users can enable and disable the library as given.
(fetch-new-theory (include-book "arithmetic-5" :dir :system) use-aritmetic-5)
(use-aritmetic-5 t)
(use-aritmetic-5 nil)
If you wish not to generate a macro, you may want to use preserve-current-theory