src/HOL/Library/Enum.thy
changeset 30458 804de935c328
parent 29961 c7849326100e
child 30663 0b6aff7451b2