doc-src/TutorialI/Misc/natsum.thy
changeset 41984 e5dba3d75e9e
parent 27168 9a9cc62932d9