src/HOL/Enum.thy
changeset 60867 86e7560e07d0
parent 60758 d8d85a8172b5
child 61076 bdc1e2f0a86a