src/HOL/Library/Char_ord.thy
changeset 77393 cb92bd1c6f8c
parent 75662 ed15f2cd4f7d
equal deleted inserted replaced
77392:467a8f987b5a 77393:cb92bd1c6f8c