src/HOL/Library/Char_nat.thy
changeset 27885 76b51cd0a37c
parent 27651 16a26996c30e
child 28562 4e74209f113e