src/HOL/Enum.thy
changeset 54574 d04e74341d43
parent 54295 45a5523d4a63
child 54890 cb892d835803