src/HOL/Library/Code_Char_chr.thy
changeset 30354 0d037d7e2a75
parent 28562 4e74209f113e
child 30663 0b6aff7451b2