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