To collect the names that have been redefined
Example and General Forms: (redefined-names state)
This function collects names that have been redefined in the current ACL2
WARNING: This function does not report names that are not explicitly redefined in the current logical world. Consider for example:
(encapsulate () (defun foo () t) (local (defun foo () nil)) (defthm foo-prop (equal (foo) nil) :rule-classes nil))
If you attempt to call certify-book in the resulting world, ACL2 will appropriately refuse to do the certification:
ACL2 Error in (CERTIFY-BOOK "foo" ...): At least one command in the current ACL2 world was executed while the value of state global variable 'LD-REDEFINITION-ACTION was not nil: (DEFUN FOO NIL T) Certification is therefore not allowed in this world. You can use :ubt to undo back through this command; see :DOC ubt.
However, since the local redefinition of