src/HOL/Enum.thy
changeset 68300 cd8ab1a7a286
parent 67951 655aa11359dc
child 69064 5840724b1d71