src/HOL/Library/Enum.thy
changeset 29216 528e68bea04d
parent 29024 6cfa380af73b
child 29797 08ef36ed2f8a