doc-src/TutorialI/Recdef/Nested2.thy
changeset 10340 0a380ac80e7d
parent 10212 33fe2d701ddd
child 10654 458068404143