src/HOL/Enum.thy
changeset 61306 9dd394c866fc
parent 61169 4de9ff3ea29a
child 61799 4cf66f21b764