Theorems about Java hexadecimal digits and functions in Std/strings.
Theorem:
(defthm hex-digitp-of-char-code (equal (hex-digitp (char-code char)) (str::hex-digit-char-p char)))
Theorem:
(defthm hex-digit-listp-of-chars=>nats (equal (hex-digit-listp (chars=>nats chars)) (str::hex-digit-char-list*p chars)))