src/HOL/Library/Char_ord.thy
changeset 22520 ebe95b0242b3
parent 22483 86064f2f2188
child 22805 1166a966e7b4