src/HOL/Enum.thy
changeset 44127 7b57b9295d98
parent 41115 2c362ff5daf4
child 45117 3911cf09899a
equal deleted inserted replaced
44126:ce44e70d0c47 44127:7b57b9295d98