src/HOL/Library/Enum.thy
changeset 27656 d4f6e64ee7cc
parent 27487 c8a6ce181805
child 28245 9767dd8e1e54
equal deleted inserted replaced
27655:cf0c60e821bb 27656:d4f6e64ee7cc