doc-src/TutorialI/Recdef/Nested2.thy
changeset 10979 3da4543034e7
parent 10885 90695f46440b
child 11196 bb4ede27fcb7