src/HOL/Library/Char_ord.thy
changeset 22452 8a86fd2a1bf0
parent 21911 e29bcab0c81c
child 22483 86064f2f2188