src/HOL/Library/Enum.thy
changeset 33520 b2cb4da715f7
parent 31596 c96d7e5df659
child 33635 dcaada178c6f