doc-src/TutorialI/Recdef/Nested2.thy
changeset 9941 fe05af7ec816
parent 9940 102f2430cef9
child 10171 59d6633835fa