src/HOL/Library/Char_ord.thy
changeset 22320 d5260836d662
parent 21911 e29bcab0c81c
child 22483 86064f2f2188
equal deleted inserted replaced
22319:6f162dd72f60 22320:d5260836d662