cw-event

(in-package "ACL2")

(defsection cw-event
  :parents (event-macros)
  :short "Event form of @(tsee cw)."
  :long (topstring (p "When this macro is processed as an event,
     its arguments are passed to @(tsee cw).")
    (p "Exception: No printing is done while including a book
     or during the second pass of an @(tsee encapsulate) event.")
    (@def "cw-event"))
  (defmacro cw-event
    (str &rest args)
    `(value-triple (cw ,STR ,@ARGS) :on-skip-proofs :interactive)))