theorem-namep

(in-package "ACL2")

(define theorem-namep
  (x (wrld plist-worldp))
  :returns (yes/no booleanp)
  :parents (std/system/event-name-queries)
  :short "Recognize symbols that name theorems."
  :long (topstring-p "This function is enabled because it is meant as an abbreviation.
    Thus, theorems triggered by this function should be generally avoided.")
  (and (symbolp x) (theorem-symbolp x wrld))
  :enabled t)