src/HOL/Library/Enum.thy
changeset 29237 e90d9d51106b
parent 29024 6cfa380af73b
child 29797 08ef36ed2f8a