src/HOL/Enum.thy
changeset 63982 4c4049e3bad8
parent 63950 cdc1e59aa513
child 64290 fb5c74a58796