doc-src/TutorialI/Overview/Ordinal.thy
changeset 13258 8f394f266025
parent 13250 efd5db7dc7cc