src/HOL/Enum.thy
changeset 64829 07f209e957bc
parent 64592 7759f1766189
child 65956 639eb3617a86