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