doc-src/TutorialI/Misc/natsum.thy
changeset 10795 9e888d60d3e5
parent 10788 ea48dd8b0232
child 10971 6852682eaf16