src/HOL/Enum.thy
changeset 70491 8cac53925407
parent 69850 5f993636ac07
child 70523 1182ea5c9a6e