src/HOL/Enum.thy
changeset 58151 414deb2ef328
parent 58101 e7ebe5554281
child 58152 6fe60a9a5bad