theorem-symbol-listp

(in-package "ACL2")

(deflist theorem-symbol-listp
  (x wrld)
  :parents (std/system/event-name-queries)
  :short "Lift @(tsee theorem-symbolp) to lists."
  :guard (and (symbol-listp x) (plist-worldp wrld))
  (theorem-symbolp x wrld)
  :true-listp t)