not* is like not but is not built-in to ACL2 and is typically disabled.
This might occasionally be useful for avoiding case-splitting in theorems.
Function: not*
(defun not* (x) (declare (xargs :guard t)) (not x))
