src/HOL/Enum.thy
changeset 64990 c6a7de505796
parent 64592 7759f1766189
child 65956 639eb3617a86