src/HOL/Enum.thy
changeset 58138 3bfd12e456f4
parent 58101 e7ebe5554281
child 58152 6fe60a9a5bad