src/HOL/Enum.thy
changeset 58839 ccda99401bc8
parent 58710 7216a10d69ba
child 58889 5b7a9633cfa8