src/HOL/Enum.thy
changeset 54230 b1d955791529
parent 54148 c8cc5ab4a863
child 54295 45a5523d4a63