src/HOL/Library/Enum.thy
changeset 34889 dcaf6ec84e28
parent 33639 603320b93668
child 37601 2a4fb776ca53