src/ZF/ex/Enum.thy
changeset 4524 7399288f5dd3
parent 1478 2b8c2a7547ab
child 11354 9b80fe19407f