src/HOL/Library/Char_nat.thy
changeset 28658 a03ae929d9c0
parent 28562 4e74209f113e
child 30224 79136ce06bdb