src/HOL/Library/Char_ord.thy
changeset 67970 8c012a49293a
parent 67399 eab6ce8368fa
child 68028 1f9f973eed2a