src/HOL/Library/Enum.thy
changeset 30005 7d97e20728d4
parent 29961 c7849326100e
child 30663 0b6aff7451b2