src/HOL/Library/Char_ord.thy
changeset 25459 d1dce7d0731c
parent 23394 474ff28210c0
child 25502 9200b36280c0