src/HOL/Enum.thy
changeset 67710 cc2db3239932
parent 67613 ce654b0e6d69
child 67829 2a6ef5ba4822