src/ZF/ex/Enum.thy
changeset 8958 ba75f564726b
parent 1478 2b8c2a7547ab
child 11354 9b80fe19407f