Recognize symbols that name theorems.
(theorem-namep x wrld) → yes/no
This function is enabled because it is meant as an abbreviation. Thus, theorems triggered by this function should be generally avoided.
(defun theorem-namep (x wrld) (declare (xargs :guard (plist-worldp wrld))) (let ((__function__ 'theorem-namep)) (declare (ignorable __function__)) (and (symbolp x) (theorem-symbolp x wrld))))
(defthm booleanp-of-theorem-namep (b* ((yes/no (theorem-namep x wrld))) (booleanp yes/no)) :rule-classes :rewrite)