[STATEMENT]
lemma digit3_ascii_of_iff [simp]:
  "digit3 (String.ascii_of c) \<longleftrightarrow> digit3 c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit3 (ascii_of c) = digit3 c
[PROOF STEP]
by (simp add: String.ascii_of_def)