src/HOL/Enum.thy
changeset 71771 7c0de1eb6075
parent 71154 7db80bd16f1c
child 78099 4d9349989d94
equal deleted inserted replaced
71770:33e886e21ed4 71771:7c0de1eb6075