doc-src/TutorialI/Overview/LNCS/Ordinal.thy
changeset 43435 ae6b0c3e58a8
parent 35437 fe196f61b970