src/HOL/Library/Char_nat.thy
changeset 29401 94fd5dd918f5
parent 28562 4e74209f113e
child 30224 79136ce06bdb