src/HOL/Library/Enum.thy
changeset 40217 656bb85f01ab
parent 39302 d7728f65b353
child 40647 6e92ca8e981b
equal deleted inserted replaced
40216:366309dfaf60 40217:656bb85f01ab