src/HOL/Enum.thy
changeset 54259 71c701dc5bf9
parent 54148 c8cc5ab4a863
child 54295 45a5523d4a63