doc-src/TutorialI/Misc/natsum.thy
changeset 33224 e15ce5aeb6d5
parent 27168 9a9cc62932d9
equal deleted inserted replaced
33223:d27956b4d3b4 33224:e15ce5aeb6d5