src/HOL/Enum.thy
changeset 64876 65a247444100
parent 64592 7759f1766189
child 65956 639eb3617a86