src/HOL/Library/Char_ord.thy
changeset 29728 2a4f000d1e4d
parent 28562 4e74209f113e
child 30663 0b6aff7451b2