src/HOL/Enum.thy
changeset 69852 54243334edcf
parent 69850 5f993636ac07
child 70523 1182ea5c9a6e