src/HOL/Library/Char_ord.thy
changeset 23951 b188cac107ad
parent 23394 474ff28210c0
child 25502 9200b36280c0
equal deleted inserted replaced
23950:f54c0e339061 23951:b188cac107ad