src/HOL/Library/Enum.thy
changeset 27986 26e1a7a6695d
parent 27487 c8a6ce181805
child 28245 9767dd8e1e54