src/HOL/Enum.thy
changeset 54614 689398f0953f
parent 54295 45a5523d4a63
child 54890 cb892d835803