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