doc-src/TutorialI/Recdef/Nested2.thy
changeset 10037 0d2a6feeb634
parent 9940 102f2430cef9
child 10171 59d6633835fa