src/HOL/Library/Char_ord.thy
changeset 76043 b80f33e5323f
parent 75662 ed15f2cd4f7d
equal deleted inserted replaced
76042:e076b1b42c44 76043:b80f33e5323f