src/HOL/Library/Enum.thy
changeset 37473 013f78aed840
parent 33639 603320b93668
child 37601 2a4fb776ca53