doc-src/TutorialI/Overview/LNCS/Ordinal.thy
changeset 40887 ee8d0548c148
parent 35437 fe196f61b970