doc-src/TutorialI/Misc/natsum.thy
changeset 10865 18927bcf7aed
parent 10788 ea48dd8b0232
child 10971 6852682eaf16