src/HOL/Library/Char_ord.thy
changeset 73182 a8a8bc42d552
parent 68028 1f9f973eed2a
child 75600 6de655ccac19
equal deleted inserted replaced
73181:02422c9add5e 73182:a8a8bc42d552