src/HOL/Enum.thy
changeset 60243 5901cb4db0ae
parent 59867 58043346ca64
child 60352 d46de31a50c4