src/HOL/Enum.thy
changeset 68685 4b367da119ed
parent 67951 655aa11359dc
child 69064 5840724b1d71