doc-src/TutorialI/Recdef/Nested1.thy
changeset 9779 c71a1acffc27
parent 9754 a123a64cadeb
child 9792 bbefb6ce5cb2