src/HOL/Library/Char_nat.thy
changeset 28131 3130d7b3149d
parent 27651 16a26996c30e
child 28562 4e74209f113e