src/HOL/Enum.thy
changeset 55770 f2cf7f92c9ac
parent 55088 57c82e01022b
child 57247 8191ccf6a1bd