src/HOL/Library/Char_ord.thy
changeset 21966 edab0ecfbd7c
parent 21911 e29bcab0c81c
child 22483 86064f2f2188