src/HOL/Enum.thy
changeset 46264 f575281fb551
parent 45963 1c7e6454883e
child 46329 cf3b387ba667