src/HOL/Enum.thy
changeset 70027 94494b92d8d0
parent 69850 5f993636ac07
child 70523 1182ea5c9a6e