Fixed a brr error that had been caused by undefining HELP when removing legacy :doc support.

Details:

Added back a trivial HELP command (which was removed when removing
legacy :doc support), to avoid break-rewrite error; and it's a good
idea anyhow.  (Technical explanation: the error was caused by the
attempt to set up a ld-keyword-alias binding :standard-help in the brr
wormhole to the help macro, which no longer existed.)
Merge
Fixed handling of errors inside the break-rewrite loop and other wormholes.

Quoting :doc note-7-0:

  We have cleaned up handling of interrupts and aborts when inside the
  [break-rewrite] loop, or indeed any [wormhole]. Thanks to David
  Russinoff for bringing to our attention a case in which ACL2 quit a
  proof with ``Aborting due to an interrupt'' when in fact no
  interrupts had taken place. Here is an example where that no longer
  happens but did, previously. (For a different example, see the
  comment in the ACL2 sources definition of macro
  bind-acl2-time-limit.)

    (defun foo (x) (cons x x))
    (brr t)
    (monitor '(:definition foo) t)
    (thm (equal (foo y) z))
    (defun h (x) (declare (xargs :mode :program)) (car x))
    ; Raw Lisp error:
    (h 3)
    ; Previously, unexpected proof abort "due to interrupt":
    (thm (equal (append (append x y) x y) (append x y x y)))
Merge