src/HOL/Library/Char_ord.thy
changeset 78580 c3a3db450c80
parent 75662 ed15f2cd4f7d