Major Section: MISCELLANEOUS
(abort!) is evaluated inside of ACL2's command loop, the
current computation is aborted and control returns to the top of
the command loop, exactly as though the user had interrupted
and aborted the current computation.
(abort!) = nil. But imagine that it is
defined in such a way that it causes a stack overflow or other
resource exhaustion when called.