src/HOL/Enum.thy
changeset 54867 c21a2465cac1
parent 54295 45a5523d4a63
child 54890 cb892d835803