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