src/HOL/Enum.thy
changeset 70601 79831e40e2be
parent 70523 1182ea5c9a6e
child 71154 7db80bd16f1c