Outer-local
Support for events that are local to the outer context.
Think of outer-local as being like progn, except that the
events inside it are local to some encapsulate context above in which they are
sitting. Outer-local only works when paired with with-outer-locals, which
is essentially like (encapsulate nil ...) except that it allows
outer-local events to work.
Example:
(with-outer-locals
(defun exported-fn ...)
(local (defthm lemma ...))
(defthm exported-thm ...)
(outer-local :depth 1 (defthm book-thm ...)))
produces, essentially:
(local
(encapsulate nil
(defun exported-fn ...)
(local (defthm lemma ...))
(defthm exported-thm ...)
(defthm book-thm ...)))
(defun exported-fn ...)
(defthm exported-thm ...))
Effectively, the event marked outer-local is visible in book or
encapsulate surrounding this with-outer-locals event, but local to that
context.
The :depth argument to outer-local is optional but must occur
first if it is present. It takes a positive integer, defaulting to 1. There
must be depth nestings of with-outer-locals surrounding each
outer-local invocation in order for it to work as intended; in that case, the
events inside the outer-local are local to the context depth levels
outside it.
Note: IN-THEORY events inside outer-local probably won't act as you would
like them to, at least in the presence of nonlocal IN-THEORY events.
