Hiding an event in an encapsulation or book

Examples: (local (defthm hack1 (implies (and (acl2-numberp x) (acl2-numberp y) (equal (* x y) 1)) (equal y (/ x))))) (local (defun double-naturals-induction (a b) (cond ((and (integerp a) (integerp b) (< 0 a) (< 0 b)) (double-naturals-induction (1- a) (1- b))) (t (list a b))))) General Form: (local ev)

where `logic` and `ld-skip-proofsp` is `program` or if `ld-skip-proofsp` is `include-book`, then
`encapsulate` event or in a book, they are processed when the
encapsulation or book is checked for admissibility in `logic` mode
but are skipped when extending the host world. Such events are
thus considered ``local'' to the verification of the encapsulation or book.
The non-local events are the ones ``exported'' by the encapsulation or
book. See encapsulate for a thorough discussion. Also see local-incompatibility for a discussion of a commonly encountered problem with
such event hiding: you can't make an event local if its presence is required
to make sense of a non-local one.

Note that events that change the default defun-mode, and in
fact any events that set the `ACL2-defaults-table`, are
disallowed inside the scope of