src/HOL/Library/Enum.thy
changeset 33649 854173fcd21c
parent 33639 603320b93668
child 37601 2a4fb776ca53