A character set for
Function:
(defun ucletter/digit-chars$inline nil (declare (xargs :guard t)) 2475880041965221303554146304)
Theorem:
(defthm charset-p-of-ucletter/digit-chars (charset-p (ucletter/digit-chars)))
Theorem:
(defthm char-in-charset-p-of-ucletter/digit-chars (equal (char-in-charset-p x (ucletter/digit-chars)) (ucletter/digit-char-p x)))