doc-src/TutorialI/Overview/LNCS/Ordinal.thy
changeset 38007 f0a4aa17f23f
parent 35437 fe196f61b970