(in-package "ACL2")
(include-book "must-fail-local")
(include-book "must-succeed-star")
(must-fail-local (defthm th (natp (1+ x))))
(must-fail-local (defthm th (natp (1+ x))) :with-output-off nil)
(must-fail-local (defthm th (natp (1+ x))) :with-output-off (summary) :check-expansion t)