src/HOL/Enum.thy
changeset 67974 3f352a91b45a
parent 67951 655aa11359dc
child 69064 5840724b1d71