src/HOL/Enum.thy
changeset 65922 d2f19f05c0e9
parent 64592 7759f1766189
child 65956 639eb3617a86