src/HOL/Enum.thy
changeset 65524 0910f1733909
parent 64592 7759f1766189
child 65956 639eb3617a86