doc-src/TutorialI/Misc/natsum.thy
changeset 31795 be3e1cc5005c
parent 27168 9a9cc62932d9
equal deleted inserted replaced
31794:71af1fd6a5e4 31795:be3e1cc5005c