src/HOL/Enum.thy
changeset 70299 83774d669b51
parent 69850 5f993636ac07
child 70523 1182ea5c9a6e