src/HOL/Enum.thy
changeset 69017 0c1d7a414185
parent 67951 655aa11359dc
child 69064 5840724b1d71