src/HOL/Library/Char_ord.thy
changeset 82051 1be62b17bed9
parent 75662 ed15f2cd4f7d
equal deleted inserted replaced
82050:0f22f7b370b2 82051:1be62b17bed9