src/HOL/Library/Char_ord.thy
changeset 25297 a5d689d04426
parent 23394 474ff28210c0
child 25502 9200b36280c0
equal deleted inserted replaced
25296:c187b7422156 25297:a5d689d04426