src/HOL/Enum.thy
changeset 55370 e6be866b5f5b
parent 55088 57c82e01022b
child 57247 8191ccf6a1bd