doc-src/TutorialI/Misc/natsum.thy
changeset 10849 de981d0037ed
parent 10788 ea48dd8b0232
child 10971 6852682eaf16