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