src/HOL/Library/Enum.thy
changeset 29270 0eade173f77e
parent 29024 6cfa380af73b
child 29797 08ef36ed2f8a