Decimal integer constant of type unsigned long.
Function: ulong-dec-const
(defun ulong-dec-const (x) (declare (xargs :guard (and (natp x) (ulong-integerp x)))) (ulong-from-integer x))
Theorem: ulongp-of-ulong-dec-const
(defthm ulongp-of-ulong-dec-const (ulongp (ulong-dec-const x)))