src/HOL/Enum.thy
changeset 44843 93d0f85cfe4a
parent 41115 2c362ff5daf4
child 45117 3911cf09899a
equal deleted inserted replaced
44842:282eef2c0f77 44843:93d0f85cfe4a