src/HOL/Enum.thy
changeset 68050 7eacc812ad1c
parent 67951 655aa11359dc
child 69064 5840724b1d71