src/HOL/Library/Char_ord.thy
changeset 28182 bfd7a8700676
parent 27682 25aceefd4786
child 28562 4e74209f113e